Theorem simpl2 1190

Description: Simplification of conjunction. (Contributed by Jeff Hankins, 17-Nov-2009.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)

Assertion

Ref	Expression
simpl2	⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓)

Proof of Theorem simpl2

Step	Hyp	Ref	Expression
1		simpl 482	. 2 ⊢ ((𝜓 ∧ 𝜃) → 𝜓)
2	1	3ad2antl2 1184	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 396  df-3an 1087

This theorem is referenced by:  simpl12  1247  simpl22  1250  simpl32  1253  simp1l2  1265  simp2l2  1271  simp3l2  1277  3anandirs  1469  rspc3ev  3624  2nreu  4437  f1prex  7287  weniso  7356  ofmpteq  7701  tfisi  7857  mposn  8102  fprlem1  8299  smogt  8381  smocdmdom  8382  omeulem1  8596  nnmord  8646  nnmword  8647  naddasslem1  8708  naddasslem2  8709  difsnen  9069  enfixsn  9097  mapunen  9162  ac6sfi  9303  ordiso2  9530  wemaplem2  9562  wemapso2lem  9567  en2eqpr  10022  acndom  10066  infmap2  10233  cflim2  10278  cfsmolem  10285  coftr  10288  fin23lem26  10340  isf32lem9  10376  fin1a2lem9  10423  fin1a2lem10  10424  gchdomtri  10644  canth4  10662  gchpwdom  10685  gruima  10817  grudomon  10832  prn0  11004  distrlem4pr  11041  prlem934  11048  addcan  11420  addcan2  11421  divmulass  11917  divmulasscom  11918  ltmul1a  12085  supmul1  12205  uzsupss  12946  xaddass  13252  xleadd1a  13256  xlesubadd  13266  xmulass  13290  xlemul2a  13292  xadddilem  13297  xadddi  13298  ixxdisj  13363  ixxun  13364  ixxlb  13370  icoshftf1o  13475  icodisj  13477  ioounsn  13478  lincmb01cmp  13496  iccf1o  13497  elfz1b  13594  ssfzoulel  13750  modmuladd  13902  modaddmulmod  13927  ltexp2a  14154  leexp2  14159  ltexp2r  14161  exple1  14164  expnlbnd2  14220  mulsubdivbinom2  14245  fun2dmnop0  14479  ccatass  14562  ccatopth  14690  pfxccatin12lem2a  14701  repswpfx  14759  repswccat  14760  cshwidxmodr  14778  2cshw  14787  repsco  14815  s2f1o  14891  limsupgle  15445  limsupgre  15449  addcn2  15562  mulcn2  15564  binomrisefac  16010  dvdsval2  16225  dvdsadd2b  16274  dvdsmod  16297  oexpneg  16313  sadass  16437  gcdass  16514  rplpwr  16524  lcmass  16576  coprmdvds2  16616  rpmulgcd2  16618  rpdvds  16622  coprmprod  16623  cncongr2  16630  rpexp  16685  prmdiveq  16746  hashgcdlem  16748  odzdvds  16755  coprimeprodsq2  16769  pythagtriplem3  16778  pythagtriplem4  16779  pcdvdsb  16829  vdwnnlem1  16955  0ram  16980  ramz2  16984  ramub1lem1  16986  mremre  17575  mrieqv2d  17610  lubss  18496  lubun  18498  clatleglb  18501  clatglbss  18502  mrelatglb  18543  isnsgrp  18674  issubmnd  18712  gsumccat  18784  frmdss2  18806  submefmnd  18838  nmzsubg  19111  ghmnsgima  19185  gsmsymgreqlem1  19376  psgnunilem4  19443  odmodnn0  19486  odnncl  19491  odmod  19492  oddvds  19493  odeq  19496  odmulgid  19500  odmulgeq  19503  odbezout  19504  odf1o1  19518  odf1o2  19519  odngen  19523  gexdvdsi  19529  pgpfi1  19541  odcau  19550  subgslw  19562  fislw  19571  lsmless1x  19590  lsmless2x  19591  lsmsubm  19599  lsmmod  19621  lsmmod2  19622  efgsfo  19685  odadd1  19794  odadd2  19795  odadd  19796  lsmcomx  19802  prdscmnd  19807  gsumconst  19880  ablsimpgfindlem1  20055  srg1zr  20146  csrgbinom  20163  ring1eq0  20223  mulgass2  20234  rngisom1  20394  rhmdvdsr  20436  cntzsubrng  20493  cntzsubr  20534  isabvd  20689  rmodislmod  20802  rmodislmodOLD  20803  0lmhm  20914  lmhmvsca  20919  reslmhm2b  20928  pwssplit1  20933  pwssplit2  20934  pwssplit3  20935  lbspss  20956  lspsnat  21022  lidldvgen  21213  xrsdsreclblem  21332  cssmre  21612  obs2ss  21650  uvcresum  21714  frlmsslsp  21717  frlmup4  21722  lindff1  21741  f1lindf  21743  lsslindf  21751  islindf4  21759  issubassa  21787  evlsval2  22020  coe1subfv  22172  coe1sclmul  22188  coe1sclmul2  22190  mpomatmul  22335  mamutpos  22347  scmatscmide  22396  mavmulsolcl  22440  mulmarep1gsum2  22463  mdetdiaglem  22487  mdetdiag  22488  mdetunilem1  22501  mdetunilem3  22503  mdetunilem9  22509  maducoeval2  22529  madurid  22533  slesolinvbi  22570  cramerimplem1  22572  cramerlem1  22576  cramer  22580  cpmatel2  22602  m2cpm  22630  m2pmfzmap  22636  m2cpminvid2lem  22643  m2cpminvid2  22644  decpmatmul  22661  pmatcollpw1lem2  22664  pmatcollpw1  22665  pmatcollpw2lem  22666  pmatcollpwfi  22671  pm2mpcl  22686  mply1topmatcl  22694  mp2pm2mplem2  22696  mp2pm2mplem4  22698  mp2pm2mplem5  22699  mp2pm2mp  22700  pm2mpghmlem2  22701  pm2mpghmlem1  22702  chfacfisfcpmat  22744  topssnei  23015  cnconst2  23174  cnpresti  23179  cnprest2  23181  cnpdis  23184  cnt0  23237  cnt1  23241  cnhaus  23245  sscmp  23296  hauscmp  23298  cnconn  23313  unconn  23320  finlocfin  23411  comppfsc  23423  kgen2ss  23446  ptpjopn  23503  prdstopn  23519  ptrescn  23530  qtopss  23606  kqfvima  23621  fbssint  23729  fbasrn  23775  filuni  23776  fmss  23837  rnelfm  23844  fmufil  23850  fmco  23852  flimss2  23863  flimss1  23864  flimrest  23874  cnpflf2  23891  flfcnp  23895  supnfcls  23911  fclsss1  23913  fclsss2  23914  isfcf  23925  subgntr  23998  opnsubg  23999  cldsubg  24002  ghmcnp  24006  ustuqtop1  24133  bldisj  24291  blgt0  24292  bl2in  24293  blss2ps  24296  blss2  24297  blssps  24317  blss  24318  xmetresbl  24330  lpbl  24399  blcld  24401  stdbdmopn  24414  metcnp3  24436  metcnp  24437  metcnp2  24438  txmetcnp  24443  blval2  24458  nmoix  24633  nmoi2  24634  nmotri  24643  metdsge  24752  metdseq0  24757  iocopnst  24851  xrhmeo  24858  nmhmcn  25034  cphsqrtcl2  25101  cphsqrtcl3  25102  cssbn  25290  pjth  25354  ovoliunlem2  25419  volun  25461  mbfimaopn2  25573  iblconst  25734  limcvallem  25787  dvfval  25813  dvcnp2  25836  dvcnp2OLD  25837  dvcn  25838  deg1mul3le  26039  deg1tmle  26040  dvdsq1p  26084  idomrootle  26094  ig1peu  26096  ig1pdvds  26101  ply1term  26125  coeid3  26161  dgrmulc  26193  dvply1  26205  aaliou2  26262  efcvx  26373  tanord  26459  eflogeq  26523  logdivlti  26541  logccv  26584  recxpcl  26596  cxplea  26617  cxpeq  26679  ang180  26733  isosctrlem2  26738  cxp2lim  26896  amgm  26910  muval1  27052  dvdssqf  27057  mumullem2  27099  mumul  27100  bcmono  27197  lgsneg  27241  lgsdilem  27244  lgsdirprm  27251  lgsdir  27252  lgsdi  27254  lgsne0  27255  nolesgn2o  27591  nogesgn1o  27593  nosep1o  27601  nosep2o  27602  nosepssdm  27606  nosupres  27627  nosupbnd1lem1  27628  nosupbnd1lem4  27631  nosupbnd1lem5  27632  nosupbnd1lem6  27633  noinfres  27642  noinfbnd1lem1  27643  noinfbnd1lem4  27646  noinfbnd1lem6  27648  noinfbnd2  27651  noetasuplem3  27655  noetainflem3  27659  slelss  27821  cofsslt  27825  coinitsslt  27826  cofcutrtime  27834  addsass  27909  addsdi  28042  mulsass  28053  sltmul2  28058  divsmulw  28079  brbtwn2  28703  colinearalglem1  28704  colinearalg  28708  axcgrtr  28713  axsegconlem8  28722  axsegconlem9  28723  axsegconlem10  28724  axcontlem2  28763  axcontlem10  28771  elntg2  28783  ewlkle  29406  crctcshwlkn0lem5  29612  wwlknp  29641  wwlksnext  29691  wwlksnextproplem1  29707  wspthsnwspthsnon  29714  clwlkclwwlklem3  29798  erclwwlksym  29818  erclwwlknsym  29867  upgriseupth  30004  eucrct2eupth  30042  3cyclfrgrrn  30083  numclwwlk2lem1lem  30139  numclwwlk1lem2foa  30151  frgrregord13  30193  nvmul0or  30447  ipval2lem2  30501  lnoadd  30555  lnosub  30556  lnomul  30557  shless  31156  shlej1  31157  kbmul  31752  homco2  31774  kbass2  31914  eliccelico  32529  elicoelioo  32530  iocinioc2  32531  iocinif  32533  difioo  32534  swrdrn2  32657  swrdrn3  32658  xrge0adddir  32730  xrge0npcan  32732  isarchi2  32871  archiabl  32884  pidlnz  33027  lindssn  33033  ssmxidl  33123  pstmfval  33433  fmcncfil  33468  zrhnm  33506  qqhnm  33527  nexple  33564  volfiniune  33785  dya2iocnrect  33837  probinc  33977  cndprob01  33991  signswmnd  34125  bnj517  34452  cvmsss2  34820  cvmlift2lem10  34858  br6  35287  funsseq  35299  cgrtriv  35534  5segofs  35538  btwnouttr2  35554  btwnxfr  35588  lineext  35608  btwnconn1lem13  35631  brsegle2  35641  nn0prpwlem  35742  lindsenlbs  37023  blbnd  37195  ismtyima  37211  rrndstprj2  37239  ghomdiv  37300  grpokerinj  37301  lsatfixedN  38418  lssat  38425  lshpkrlem4  38522  cvrcon3b  38686  atlen0  38719  atcvreq0  38723  atnle  38726  atlatmstc  38728  atlatle  38729  cvlcvr1  38748  hlsupr2  38797  hlrelat2  38813  cvrexchlem  38829  lnnat  38837  atcvrj2b  38842  3dimlem3  38871  3dim1  38877  1cvrjat  38885  llni  38918  llni2  38922  llnexatN  38931  2llnmat  38934  lplni  38942  2atnelpln  38954  llncvrlpln2  38967  2llnmj  38970  lplnexatN  38973  lplnexllnN  38974  2llnm3N  38979  lvoli  38985  lvoli3  38987  lvolnle3at  38992  islvol2aN  39002  4atlem4a  39009  4atlem4b  39010  4atlem11  39019  lplncvrlvol2  39025  2lplnmj  39032  islinei  39150  linepmap  39185  lnjatN  39190  lncvrat  39192  lncmp  39193  elpaddn0  39210  elpaddatriN  39213  elpaddat  39214  paddcom  39223  paddss2  39228  paddss12  39229  paddasslem4  39233  paddasslem9  39238  paddasslem10  39239  pmodl42N  39261  pmapjoin  39262  llnmod1i2  39270  polcon2bN  39330  pclfinclN  39360  poml4N  39363  poml6N  39365  osumcllem1N  39366  osumcllem2N  39367  osumcllem11N  39376  osumclN  39377  pmapojoinN  39378  pexmidlem2N  39381  pexmidlem3N  39382  pexmidlem4N  39383  pexmidlem6N  39385  pexmidlem7N  39386  pl42lem2N  39390  pl42lem3N  39391  pl42lem4N  39392  pl42N  39393  lhprelat3N  39450  4atex  39486  lauteq  39505  lautco  39507  ltrncoidN  39538  ltrneq2  39558  ltrnideq  39585  trlnle  39596  trlval3  39597  cdlemc  39607  cdlemd9  39616  cdlemd  39617  cdleme21j  39746  cdleme21  39747  cdleme29ex  39784  cdlemefr27cl  39813  cdlemefs27cl  39823  cdleme32d  39854  cdleme32f  39856  cdleme35h2  39867  cdleme40m  39877  cdleme17d3  39906  cdleme48fvg  39910  cdlemeg46fvcl  39916  cdlemeg46fgN  39944  cdleme48fgv  39948  cdleme50trn3  39963  cdlemb3  40016  cdlemg8  40041  cdlemg11a  40047  cdlemg15a  40065  cdlemg15  40066  cdlemg16  40067  cdlemg16z  40069  cdlemg17dN  40073  cdlemg24  40098  cdlemg37  40099  cdlemg29  40115  cdlemg33b  40117  cdlemg38  40125  cdlemg40  40127  trlco  40137  cdlemg44b  40142  ltrncom  40148  trljco  40150  tendococl  40182  tendoplcl  40191  tendoplcom  40192  cdlemj2  40232  tendoid0  40235  tendo1ne0  40238  cdlemk25-3  40314  cdlemk36  40323  cdlemkid4  40344  cdlemk19x  40353  cdlemk53  40367  cdlemk56  40381  cdleml5N  40390  tendospcanN  40433  cdlemm10N  40528  dihord6apre  40666  dihord  40674  dihmeetlem1N  40700  dihglblem2N  40704  dihmeetlem2N  40709  dihmeetbN  40713  dihmeetlem5  40718  dihmeetlem6  40719  dihmeetlem7N  40720  dihmeetlem10N  40726  dihmeetlem12N  40728  dihmeetlem16N  40732  dihmeetlem17N  40733  dihmeetlem18N  40734  dihmeetALTN  40737  dihlspsnssN  40742  dvh3dim2  40858  dvh3dim3N  40859  lcfrlem16  40968  mapdrvallem2  41055  mapdh8ad  41189  hgmapvvlem3  41335  sticksstones1  41550  sticksstones2  41551  resubcan2  41865  diophrw  42101  eldioph2lem1  42102  diophrex  42117  rencldnfi  42163  pellexlem2  42172  pellqrexplicit  42219  infmrgelbi  42220  pellfundglb  42227  pellfund14gap  42229  rmxycomplete  42260  congadd  42309  acongeq  42326  jm2.19  42336  jm2.23  42339  jm2.20nn  42340  jm2.27  42351  jm3.1  42363  lnmepi  42431  lmhmlnmsplit  42433  hbtlem2  42470  dgraa0p  42495  proot1hash  42545  iocunico  42562  iocinico  42563  oasubex  42638  cantnf2  42677  onmcl  42683  omcl2  42685  nadd2rabex  42738  nadd1rabtr  42740  nadd1rabex  42742  fzunt  42808  relexpxpmin  43070  ntrclsk3  43423  grur1cld  43592  ismnu  43621  grumnudlem  43645  ismnushort  43661  rfcnnnub  44321  uzwo4  44340  wessf1ornlem  44481  supxrge  44643  infleinflem2  44676  iccintsng  44831  climsuse  44919  lptre2pt  44951  limcleqr  44955  0ellimcdiv  44960  fnlimfvre  44985  dvnprodlem1  45257  volioc  45283  stoweidlem17  45328  stoweidlem19  45330  stoweidlem20  45331  stoweidlem22  45333  stoweidlem28  45339  stoweidlem34  45345  stoweidlem44  45355  stoweidlem60  45371  wallispilem3  45378  fourierdlem42  45460  fourierdlem48  45465  fourierdlem51  45468  fourierdlem54  45471  fourierdlem74  45491  fourierdlem77  45494  fourierdlem87  45504  fourierdlem97  45514  ioorrnopnlem  45615  ovnsubaddlem2  45882  smfinflem  46128  fsupdm  46153  finfdm  46157  eluzge0nn0  46615  fzopredsuc  46626  fzoopth  46630  imasetpreimafvbijlemfv  46665  lighneallem4  46873  oexpnegALTV  46940  oexpnegnz  46941  tgblthelfgott  47078  rmsupp0  47355  rmsuppss  47357  lincresunit3lem3  47465  lincresunit3lem2  47471  lindssnlvec  47477  fdivmptf  47537  refdivmptf  47538  elbigolo1  47553  rrx2linest  47738  itsclc0lem1  47752  itsclc0lem2  47753  itsclc0yqsollem1  47758  itsclc0b  47768