Theorem simpl2 1202

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 485	. 2 ⊢ ((𝜓 ∧ 𝜃) → 𝜓)
2	1	3ad2antl2 1196	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1095

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 209  df-an 399  df-3an 1097

This theorem is referenced by:  simpl12  1259  simpl22  1262  simpl32  1265  simp1l2  1277  simp2l2  1283  simp3l2  1289  3anandirs  1487  rspc3ev  3593  2nreu  4392  f1prex  7257  weniso  7327  ofmpteq  7672  tfisi  7828  mposn  8070  fprlem1  8269  smogt  8326  smocdmdom  8327  omeulem1  8539  nnmord  8590  nnmword  8591  naddasslem1  8653  naddasslem2  8654  difsnen  9020  enfixsn  9047  mapunen  9107  ac6sfi  9217  ordiso2  9453  wemaplem2  9485  wemapso2lem  9490  en2eqpr  9953  acndom  9997  infmap2  10163  cflim2  10210  cfsmolem  10217  coftr  10220  fin23lem26  10272  isf32lem9  10308  fin1a2lem9  10355  fin1a2lem10  10356  gchdomtri  10577  canth4  10595  gchpwdom  10618  gruima  10750  grudomon  10765  prn0  10937  distrlem4pr  10974  prlem934  10981  addcan  11357  addcan2  11358  divmulass  11858  divmulasscom  11859  ltmul1a  12030  supmul1  12151  uzsupss  12931  xaddass  13242  xleadd1a  13246  xlesubadd  13256  xmulass  13280  xlemul2a  13282  xadddilem  13287  xadddi  13288  ixxdisj  13354  ixxun  13355  ixxlb  13361  icoshftf1o  13468  icodisj  13470  ioounsn  13471  lincmb01cmp  13489  iccf1o  13490  elfz1b  13588  ssfzoulel  13756  fzoopth  13758  modmuladd  13916  modaddmulmod  13941  ltexp2a  14169  leexp2  14174  ltexp2r  14176  exple1  14180  expnlbnd2  14237  mulsubdivbinom2  14265  fun2dmnop0  14507  ccatass  14592  ccatopth  14719  pfxccatin12lem2a  14730  repswpfx  14788  repswccat  14789  cshwidxmodr  14807  2cshw  14816  repsco  14843  s2f1o  14919  limsupgle  15480  limsupgre  15484  addcn2  15597  mulcn2  15599  binomrisefac  16048  dvdsval2  16265  dvdsadd2b  16316  dvdsmod  16339  oexpneg  16355  sadass  16481  gcdass  16557  rplpwr  16568  lcmass  16624  coprmdvds2  16664  rpmulgcd2  16666  rpdvds  16670  coprmprod  16671  cncongr2  16678  rpexp  16733  prmdiveq  16797  hashgcdlem  16799  odzdvds  16807  coprimeprodsq2  16821  pythagtriplem3  16830  pythagtriplem4  16831  pcdvdsb  16881  vdwnnlem1  17007  0ram  17032  ramz2  17036  ramub1lem1  17038  mremre  17608  mrieqv2d  17647  lubss  18521  lubun  18523  clatleglb  18526  clatglbss  18527  mrelatglb  18568  isnsgrp  18733  issubmnd  18771  gsumccat  18851  frmdss2  18873  submefmnd  18905  nmzsubg  19182  ghmnsgima  19256  gsmsymgreqlem1  19446  psgnunilem4  19513  odmodnn0  19556  odnncl  19561  odmod  19562  oddvds  19563  odeq  19566  odmulgid  19570  odmulgeq  19573  odbezout  19574  odf1o1  19588  odf1o2  19589  odngen  19593  gexdvdsi  19599  pgpfi1  19611  odcau  19620  subgslw  19632  fislw  19641  lsmless1x  19660  lsmless2x  19661  lsmsubm  19669  lsmmod  19691  lsmmod2  19692  efgsfo  19755  odadd1  19864  odadd2  19865  odadd  19866  lsmcomx  19872  prdscmnd  19877  gsumconst  19950  ablsimpgfindlem1  20125  srg1zr  20237  csrgbinom  20254  ring1eq0  20320  mulgass2  20331  rngisom1  20487  rhmdvdsr  20530  cntzsubrng  20589  cntzsubr  20628  isabvd  20834  rmodislmod  20970  0lmhm  21080  lmhmvsca  21085  reslmhm2b  21094  pwssplit1  21099  pwssplit2  21100  pwssplit3  21101  lbspss  21122  lspsnat  21188  lidldvgen  21377  xrsdsreclblem  21438  cssmre  21718  obs2ss  21754  uvcresum  21818  frlmsslsp  21821  frlmup4  21826  lindff1  21845  f1lindf  21847  lsslindf  21855  islindf4  21863  issubassa  21892  evlsval2  22113  coe1subfv  22302  coe1sclmul  22318  coe1sclmul2  22320  mpomatmul  22479  mamutpos  22491  scmatscmide  22540  mavmulsolcl  22584  mulmarep1gsum2  22607  mdetdiaglem  22631  mdetdiag  22632  mdetunilem1  22645  mdetunilem3  22647  mdetunilem9  22653  maducoeval2  22673  madurid  22677  slesolinvbi  22714  cramerimplem1  22716  cramerlem1  22720  cramer  22724  cpmatel2  22746  m2cpm  22774  m2pmfzmap  22780  m2cpminvid2lem  22787  m2cpminvid2  22788  decpmatmul  22805  pmatcollpw1lem2  22808  pmatcollpw1  22809  pmatcollpw2lem  22810  pmatcollpwfi  22815  pm2mpcl  22830  mply1topmatcl  22838  mp2pm2mplem2  22840  mp2pm2mplem4  22842  mp2pm2mplem5  22843  mp2pm2mp  22844  pm2mpghmlem2  22845  pm2mpghmlem1  22846  chfacfisfcpmat  22888  topssnei  23157  cnconst2  23316  cnpresti  23321  cnprest2  23323  cnpdis  23326  cnt0  23379  cnt1  23383  cnhaus  23387  sscmp  23438  hauscmp  23440  cnconn  23455  unconn  23462  finlocfin  23553  comppfsc  23565  kgen2ss  23588  ptpjopn  23645  prdstopn  23661  ptrescn  23672  qtopss  23748  kqfvima  23763  fbssint  23871  fbasrn  23917  filuni  23918  fmss  23979  rnelfm  23986  fmufil  23992  fmco  23994  flimss2  24005  flimss1  24006  flimrest  24016  cnpflf2  24033  flfcnp  24037  supnfcls  24053  fclsss1  24055  fclsss2  24056  isfcf  24067  subgntr  24140  opnsubg  24141  cldsubg  24144  ghmcnp  24148  ustuqtop1  24274  bldisj  24431  blgt0  24432  bl2in  24433  blss2ps  24436  blss2  24437  blssps  24457  blss  24458  xmetresbl  24470  lpbl  24536  blcld  24538  stdbdmopn  24551  metcnp3  24573  metcnp  24574  metcnp2  24575  txmetcnp  24580  blval2  24595  nmoix  24762  nmoi2  24763  nmotri  24772  metdsge  24883  metdseq0  24888  iocopnst  24975  xrhmeo  24981  nmhmcn  25155  cphsqrtcl2  25221  cphsqrtcl3  25222  cssbn  25410  pjth  25474  ovoliunlem2  25538  volun  25580  mbfimaopn2  25692  iblconst  25853  limcvallem  25906  dvfval  25932  dvcnp2  25955  dvcn  25956  deg1mul3le  26150  deg1tmle  26151  dvdsq1p  26196  idomrootle  26206  ig1peu  26208  ig1pdvds  26213  ply1term  26237  coeid3  26273  dgrmulc  26304  dvply1  26318  aaliou2  26374  efcvx  26482  tanord  26573  eflogeq  26637  logdivlti  26655  logccv  26698  recxpcl  26710  cxplea  26731  cxpeq  26792  ang180  26849  isosctrlem2  26854  cxp2lim  27011  amgm  27025  muval1  27167  dvdssqf  27172  mumullem2  27214  mumul  27215  bcmono  27311  lgsneg  27355  lgsdilem  27358  lgsdirprm  27365  lgsdir  27366  lgsdi  27368  lgsne0  27369  nolesgn2o  27705  nogesgn1o  27707  nosep1o  27715  nosep2o  27716  nosepssdm  27720  nosupres  27741  nosupbnd1lem1  27742  nosupbnd1lem4  27745  nosupbnd1lem5  27746  nosupbnd1lem6  27747  noinfres  27756  noinfbnd1lem1  27757  noinfbnd1lem4  27760  noinfbnd1lem6  27762  noinfbnd2  27765  noetasuplem3  27769  noetainflem3  27773  leslss  27972  cofslts  27981  coinitslts  27982  cofcutrtime  27990  addsass  28068  addsdi  28218  mulsass  28229  ltmuls2  28234  divmulsw  28256  bdayfinbndlem1  28530  z12bdaylem  28547  brbtwn2  29045  colinearalglem1  29046  colinearalg  29050  axcgrtr  29055  axsegconlem8  29064  axsegconlem9  29065  axsegconlem10  29066  axcontlem2  29105  axcontlem10  29113  elntg2  29125  ewlkle  29745  crctcshwlkn0lem5  29953  wwlknp  29982  wwlksnext  30032  wwlksnextproplem1  30048  wspthsnwspthsnon  30055  clwlkclwwlklem3  30142  erclwwlksym  30162  erclwwlknsym  30211  upgriseupth  30348  eucrct2eupth  30386  3cyclfrgrrn  30427  numclwwlk2lem1lem  30483  numclwwlk1lem2foa  30495  frgrregord13  30537  nvmul0or  30792  ipval2lem2  30846  lnoadd  30900  lnosub  30901  lnomul  30902  shless  31501  shlej1  31502  kbmul  32097  homco2  32119  kbass2  32259  eliccelico  32922  elicoelioo  32923  iocinioc2  32924  iocinif  32926  difioo  32927  nexple  32989  swrdrn2  33086  swrdrn3  33087  xrge0adddir  33150  xrge0npcan  33152  isarchi2  33319  archiabl  33332  pidlnz  33516  lindssn  33518  ssmxidl  33616  pstmfval  34147  fmcncfil  34182  zrhnm  34218  qqhnm  34241  volfiniune  34481  dya2iocnrect  34532  probinc  34672  cndprob01  34686  signswmnd  34808  bnj517  35137  cvmsss2  35572  cvmlift2lem10  35610  br6  36055  funsseq  36066  cgrtriv  36300  5segofs  36304  btwnouttr2  36320  btwnxfr  36354  lineext  36374  btwnconn1lem13  36397  brsegle2  36407  nn0prpwlem  36630  weiunpo  36773  weiunso  36774  weiunfr  36775  weiunse  36776  axtcond  36786  lindsenlbs  38062  blbnd  38234  ismtyima  38250  rrndstprj2  38278  ghomdiv  38339  grpokerinj  38340  lsatfixedN  39581  lssat  39588  lshpkrlem4  39685  cvrcon3b  39849  atlen0  39882  atcvreq0  39886  atnle  39889  atlatmstc  39891  atlatle  39892  cvlcvr1  39911  hlsupr2  39959  hlrelat2  39975  cvrexchlem  39991  lnnat  39999  atcvrj2b  40004  3dimlem3  40033  3dim1  40039  1cvrjat  40047  llni  40080  llni2  40084  llnexatN  40093  2llnmat  40096  lplni  40104  2atnelpln  40116  llncvrlpln2  40129  2llnmj  40132  lplnexatN  40135  lplnexllnN  40136  2llnm3N  40141  lvoli  40147  lvoli3  40149  lvolnle3at  40154  islvol2aN  40164  4atlem4a  40171  4atlem4b  40172  4atlem11  40181  lplncvrlvol2  40187  2lplnmj  40194  islinei  40312  linepmap  40347  lnjatN  40352  lncvrat  40354  lncmp  40355  elpaddn0  40372  elpaddatriN  40375  elpaddat  40376  paddcom  40385  paddss2  40390  paddss12  40391  paddasslem4  40395  paddasslem9  40400  paddasslem10  40401  pmodl42N  40423  pmapjoin  40424  llnmod1i2  40432  polcon2bN  40492  pclfinclN  40522  poml4N  40525  poml6N  40527  osumcllem1N  40528  osumcllem2N  40529  osumcllem11N  40538  osumclN  40539  pmapojoinN  40540  pexmidlem2N  40543  pexmidlem3N  40544  pexmidlem4N  40545  pexmidlem6N  40547  pexmidlem7N  40548  pl42lem2N  40552  pl42lem3N  40553  pl42lem4N  40554  pl42N  40555  lhprelat3N  40612  4atex  40648  lauteq  40667  lautco  40669  ltrncoidN  40700  ltrneq2  40720  ltrnideq  40747  trlnle  40758  trlval3  40759  cdlemc  40769  cdlemd9  40778  cdlemd  40779  cdleme21j  40908  cdleme21  40909  cdleme29ex  40946  cdlemefr27cl  40975  cdlemefs27cl  40985  cdleme32d  41016  cdleme32f  41018  cdleme35h2  41029  cdleme40m  41039  cdleme17d3  41068  cdleme48fvg  41072  cdlemeg46fvcl  41078  cdlemeg46fgN  41106  cdleme48fgv  41110  cdleme50trn3  41125  cdlemb3  41178  cdlemg8  41203  cdlemg11a  41209  cdlemg15a  41227  cdlemg15  41228  cdlemg16  41229  cdlemg16z  41231  cdlemg17dN  41235  cdlemg24  41260  cdlemg37  41261  cdlemg29  41277  cdlemg33b  41279  cdlemg38  41287  cdlemg40  41289  trlco  41299  cdlemg44b  41304  ltrncom  41310  trljco  41312  tendococl  41344  tendoplcl  41353  tendoplcom  41354  cdlemj2  41394  tendoid0  41397  tendo1ne0  41400  cdlemk25-3  41476  cdlemk36  41485  cdlemkid4  41506  cdlemk19x  41515  cdlemk53  41529  cdlemk56  41543  cdleml5N  41552  tendospcanN  41595  cdlemm10N  41690  dihord6apre  41828  dihord  41836  dihmeetlem1N  41862  dihglblem2N  41866  dihmeetlem2N  41871  dihmeetbN  41875  dihmeetlem5  41880  dihmeetlem6  41881  dihmeetlem7N  41882  dihmeetlem10N  41888  dihmeetlem12N  41890  dihmeetlem16N  41894  dihmeetlem17N  41895  dihmeetlem18N  41896  dihmeetALTN  41899  dihlspsnssN  41904  dvh3dim2  42020  dvh3dim3N  42021  lcfrlem16  42130  mapdrvallem2  42217  mapdh8ad  42351  hgmapvvlem3  42497  sticksstones1  42711  sticksstones2  42712  aks6d1c6isolem1  42739  resubcan2  42945  diophrw  43288  eldioph2lem1  43289  diophrex  43304  rencldnfi  43346  pellexlem2  43355  pellqrexplicit  43402  infmrgelbi  43403  pellfundglb  43410  pellfund14gap  43412  rmxycomplete  43442  congadd  43491  acongeq  43508  jm2.19  43518  jm2.23  43521  jm2.20nn  43522  jm2.27  43533  jm3.1  43545  lnmepi  43610  lmhmlnmsplit  43612  hbtlem2  43649  dgraa0p  43674  proot1hash  43720  iocunico  43736  iocinico  43737  oasubex  43811  cantnf2  43850  onmcl  43856  omcl2  43858  nadd2rabex  43911  nadd1rabtr  43913  nadd1rabex  43915  fzunt  43979  relexpxpmin  44241  ntrclsk3  44594  grur1cld  44756  ismnu  44785  grumnudlem  44809  ismnushort  44825  rfcnnnub  45564  uzwo4  45581  wessf1ornlem  45711  supxrge  45862  infleinflem2  45894  iccintsng  46047  climsuse  46132  lptre2pt  46162  limcleqr  46166  0ellimcdiv  46171  fnlimfvre  46196  dvnprodlem1  46468  volioc  46494  stoweidlem17  46539  stoweidlem19  46541  stoweidlem20  46542  stoweidlem22  46544  stoweidlem28  46550  stoweidlem34  46556  stoweidlem44  46566  stoweidlem60  46582  wallispilem3  46589  fourierdlem42  46671  fourierdlem48  46676  fourierdlem51  46679  fourierdlem54  46682  fourierdlem74  46702  fourierdlem77  46705  fourierdlem87  46715  fourierdlem97  46725  ioorrnopnlem  46826  ovnsubaddlem2  47093  smfinflem  47339  fsupdm  47364  finfdm  47368  eluzge0nn0  47854  fzopredsuc  47866  imasetpreimafvbijlemfv  47956  lighneallem4  48167  oexpnegALTV  48247  oexpnegnz  48248  tgblthelfgott  48385  clnbgrgrim  48504  isubgr3stgrlem3  48538  rmsupp0  48938  rmsuppss  48940  lincresunit3lem3  49044  lincresunit3lem2  49050  lindssnlvec  49056  fdivmptf  49111  refdivmptf  49112  elbigolo1  49127  rrx2linest  49312  itsclc0lem1  49326  itsclc0lem2  49327  itsclc0yqsollem1  49332  itsclc0b  49342  setc1onsubc  50171