Theorem simpl2 1194

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 1188	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓)

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

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  simpl12  1251  simpl22  1254  simpl32  1257  simp1l2  1269  simp2l2  1275  simp3l2  1281  3anandirs  1475  rspc3ev  3595  2nreu  4398  f1prex  7240  weniso  7310  ofmpteq  7655  tfisi  7811  mposn  8055  fprlem1  8252  smogt  8309  smocdmdom  8310  omeulem1  8519  nnmord  8570  nnmword  8571  naddasslem1  8632  naddasslem2  8633  difsnen  8999  enfixsn  9026  mapunen  9086  ac6sfi  9196  ordiso2  9432  wemaplem2  9464  wemapso2lem  9469  en2eqpr  9929  acndom  9973  infmap2  10139  cflim2  10185  cfsmolem  10192  coftr  10195  fin23lem26  10247  isf32lem9  10283  fin1a2lem9  10330  fin1a2lem10  10331  gchdomtri  10552  canth4  10570  gchpwdom  10593  gruima  10725  grudomon  10740  prn0  10912  distrlem4pr  10949  prlem934  10956  addcan  11329  addcan2  11330  divmulass  11831  divmulasscom  11832  ltmul1a  12002  supmul1  12123  uzsupss  12865  xaddass  13176  xleadd1a  13180  xlesubadd  13190  xmulass  13214  xlemul2a  13216  xadddilem  13221  xadddi  13222  ixxdisj  13288  ixxun  13289  ixxlb  13295  icoshftf1o  13402  icodisj  13404  ioounsn  13405  lincmb01cmp  13423  iccf1o  13424  elfz1b  13521  ssfzoulel  13688  fzoopth  13690  modmuladd  13848  modaddmulmod  13873  ltexp2a  14101  leexp2  14106  ltexp2r  14108  exple1  14112  expnlbnd2  14169  mulsubdivbinom2  14197  fun2dmnop0  14439  ccatass  14524  ccatopth  14651  pfxccatin12lem2a  14662  repswpfx  14720  repswccat  14721  cshwidxmodr  14739  2cshw  14748  repsco  14775  s2f1o  14851  limsupgle  15412  limsupgre  15416  addcn2  15529  mulcn2  15531  binomrisefac  15977  dvdsval2  16194  dvdsadd2b  16245  dvdsmod  16268  oexpneg  16284  sadass  16410  gcdass  16486  rplpwr  16497  lcmass  16553  coprmdvds2  16593  rpmulgcd2  16595  rpdvds  16599  coprmprod  16600  cncongr2  16607  rpexp  16661  prmdiveq  16725  hashgcdlem  16727  odzdvds  16735  coprimeprodsq2  16749  pythagtriplem3  16758  pythagtriplem4  16759  pcdvdsb  16809  vdwnnlem1  16935  0ram  16960  ramz2  16964  ramub1lem1  16966  mremre  17535  mrieqv2d  17574  lubss  18448  lubun  18450  clatleglb  18453  clatglbss  18454  mrelatglb  18495  isnsgrp  18660  issubmnd  18698  gsumccat  18778  frmdss2  18800  submefmnd  18832  nmzsubg  19106  ghmnsgima  19181  gsmsymgreqlem1  19371  psgnunilem4  19438  odmodnn0  19481  odnncl  19486  odmod  19487  oddvds  19488  odeq  19491  odmulgid  19495  odmulgeq  19498  odbezout  19499  odf1o1  19513  odf1o2  19514  odngen  19518  gexdvdsi  19524  pgpfi1  19536  odcau  19545  subgslw  19557  fislw  19566  lsmless1x  19585  lsmless2x  19586  lsmsubm  19594  lsmmod  19616  lsmmod2  19617  efgsfo  19680  odadd1  19789  odadd2  19790  odadd  19791  lsmcomx  19797  prdscmnd  19802  gsumconst  19875  ablsimpgfindlem1  20050  srg1zr  20162  csrgbinom  20179  ring1eq0  20245  mulgass2  20256  rngisom1  20414  rhmdvdsr  20453  cntzsubrng  20512  cntzsubr  20551  isabvd  20757  rmodislmod  20893  0lmhm  21004  lmhmvsca  21009  reslmhm2b  21018  pwssplit1  21023  pwssplit2  21024  pwssplit3  21025  lbspss  21046  lspsnat  21112  lidldvgen  21301  xrsdsreclblem  21379  cssmre  21660  obs2ss  21696  uvcresum  21760  frlmsslsp  21763  frlmup4  21768  lindff1  21787  f1lindf  21789  lsslindf  21797  islindf4  21805  issubassa  21834  evlsval2  22054  coe1subfv  22220  coe1sclmul  22236  coe1sclmul2  22238  mpomatmul  22402  mamutpos  22414  scmatscmide  22463  mavmulsolcl  22507  mulmarep1gsum2  22530  mdetdiaglem  22554  mdetdiag  22555  mdetunilem1  22568  mdetunilem3  22570  mdetunilem9  22576  maducoeval2  22596  madurid  22600  slesolinvbi  22637  cramerimplem1  22639  cramerlem1  22643  cramer  22647  cpmatel2  22669  m2cpm  22697  m2pmfzmap  22703  m2cpminvid2lem  22710  m2cpminvid2  22711  decpmatmul  22728  pmatcollpw1lem2  22731  pmatcollpw1  22732  pmatcollpw2lem  22733  pmatcollpwfi  22738  pm2mpcl  22753  mply1topmatcl  22761  mp2pm2mplem2  22763  mp2pm2mplem4  22765  mp2pm2mplem5  22766  mp2pm2mp  22767  pm2mpghmlem2  22768  pm2mpghmlem1  22769  chfacfisfcpmat  22811  topssnei  23080  cnconst2  23239  cnpresti  23244  cnprest2  23246  cnpdis  23249  cnt0  23302  cnt1  23306  cnhaus  23310  sscmp  23361  hauscmp  23363  cnconn  23378  unconn  23385  finlocfin  23476  comppfsc  23488  kgen2ss  23511  ptpjopn  23568  prdstopn  23584  ptrescn  23595  qtopss  23671  kqfvima  23686  fbssint  23794  fbasrn  23840  filuni  23841  fmss  23902  rnelfm  23909  fmufil  23915  fmco  23917  flimss2  23928  flimss1  23929  flimrest  23939  cnpflf2  23956  flfcnp  23960  supnfcls  23976  fclsss1  23978  fclsss2  23979  isfcf  23990  subgntr  24063  opnsubg  24064  cldsubg  24067  ghmcnp  24071  ustuqtop1  24197  bldisj  24354  blgt0  24355  bl2in  24356  blss2ps  24359  blss2  24360  blssps  24380  blss  24381  xmetresbl  24393  lpbl  24459  blcld  24461  stdbdmopn  24474  metcnp3  24496  metcnp  24497  metcnp2  24498  txmetcnp  24503  blval2  24518  nmoix  24685  nmoi2  24686  nmotri  24695  metdsge  24806  metdseq0  24811  iocopnst  24905  xrhmeo  24912  nmhmcn  25088  cphsqrtcl2  25154  cphsqrtcl3  25155  cssbn  25343  pjth  25407  ovoliunlem2  25472  volun  25514  mbfimaopn2  25626  iblconst  25787  limcvallem  25840  dvfval  25866  dvcnp2  25889  dvcnp2OLD  25890  dvcn  25891  deg1mul3le  26090  deg1tmle  26091  dvdsq1p  26136  idomrootle  26146  ig1peu  26148  ig1pdvds  26153  ply1term  26177  coeid3  26213  dgrmulc  26245  dvply1  26259  aaliou2  26316  efcvx  26427  tanord  26515  eflogeq  26579  logdivlti  26597  logccv  26640  recxpcl  26652  cxplea  26673  cxpeq  26735  ang180  26792  isosctrlem2  26797  cxp2lim  26955  amgm  26969  muval1  27111  dvdssqf  27116  mumullem2  27158  mumul  27159  bcmono  27256  lgsneg  27300  lgsdilem  27303  lgsdirprm  27310  lgsdir  27311  lgsdi  27313  lgsne0  27314  nolesgn2o  27651  nogesgn1o  27653  nosep1o  27661  nosep2o  27662  nosepssdm  27666  nosupres  27687  nosupbnd1lem1  27688  nosupbnd1lem4  27691  nosupbnd1lem5  27692  nosupbnd1lem6  27693  noinfres  27702  noinfbnd1lem1  27703  noinfbnd1lem4  27706  noinfbnd1lem6  27708  noinfbnd2  27711  noetasuplem3  27715  noetainflem3  27719  leslss  27917  cofslts  27926  coinitslts  27927  cofcutrtime  27935  addsass  28013  addsdi  28163  mulsass  28174  ltmuls2  28179  divmulsw  28201  bdayfinbndlem1  28475  z12bdaylem  28492  brbtwn2  28990  colinearalglem1  28991  colinearalg  28995  axcgrtr  29000  axsegconlem8  29009  axsegconlem9  29010  axsegconlem10  29011  axcontlem2  29050  axcontlem10  29058  elntg2  29070  ewlkle  29691  crctcshwlkn0lem5  29899  wwlknp  29928  wwlksnext  29978  wwlksnextproplem1  29994  wspthsnwspthsnon  30001  clwlkclwwlklem3  30088  erclwwlksym  30108  erclwwlknsym  30157  upgriseupth  30294  eucrct2eupth  30332  3cyclfrgrrn  30373  numclwwlk2lem1lem  30429  numclwwlk1lem2foa  30441  frgrregord13  30483  nvmul0or  30737  ipval2lem2  30791  lnoadd  30845  lnosub  30846  lnomul  30847  shless  31446  shlej1  31447  kbmul  32042  homco2  32064  kbass2  32204  eliccelico  32867  elicoelioo  32868  iocinioc2  32869  iocinif  32871  difioo  32872  nexple  32935  swrdrn2  33046  swrdrn3  33047  xrge0adddir  33110  xrge0npcan  33112  isarchi2  33278  archiabl  33291  pidlnz  33468  lindssn  33470  ssmxidl  33566  pstmfval  34073  fmcncfil  34108  zrhnm  34144  qqhnm  34167  volfiniune  34407  dya2iocnrect  34458  probinc  34598  cndprob01  34612  signswmnd  34734  bnj517  35060  cvmsss2  35487  cvmlift2lem10  35525  br6  35970  funsseq  35981  cgrtriv  36215  5segofs  36219  btwnouttr2  36235  btwnxfr  36269  lineext  36289  btwnconn1lem13  36312  brsegle2  36322  nn0prpwlem  36535  weiunpo  36678  weiunso  36679  weiunfr  36680  weiunse  36681  lindsenlbs  37855  blbnd  38027  ismtyima  38043  rrndstprj2  38071  ghomdiv  38132  grpokerinj  38133  lsatfixedN  39374  lssat  39381  lshpkrlem4  39478  cvrcon3b  39642  atlen0  39675  atcvreq0  39679  atnle  39682  atlatmstc  39684  atlatle  39685  cvlcvr1  39704  hlsupr2  39752  hlrelat2  39768  cvrexchlem  39784  lnnat  39792  atcvrj2b  39797  3dimlem3  39826  3dim1  39832  1cvrjat  39840  llni  39873  llni2  39877  llnexatN  39886  2llnmat  39889  lplni  39897  2atnelpln  39909  llncvrlpln2  39922  2llnmj  39925  lplnexatN  39928  lplnexllnN  39929  2llnm3N  39934  lvoli  39940  lvoli3  39942  lvolnle3at  39947  islvol2aN  39957  4atlem4a  39964  4atlem4b  39965  4atlem11  39974  lplncvrlvol2  39980  2lplnmj  39987  islinei  40105  linepmap  40140  lnjatN  40145  lncvrat  40147  lncmp  40148  elpaddn0  40165  elpaddatriN  40168  elpaddat  40169  paddcom  40178  paddss2  40183  paddss12  40184  paddasslem4  40188  paddasslem9  40193  paddasslem10  40194  pmodl42N  40216  pmapjoin  40217  llnmod1i2  40225  polcon2bN  40285  pclfinclN  40315  poml4N  40318  poml6N  40320  osumcllem1N  40321  osumcllem2N  40322  osumcllem11N  40331  osumclN  40332  pmapojoinN  40333  pexmidlem2N  40336  pexmidlem3N  40337  pexmidlem4N  40338  pexmidlem6N  40340  pexmidlem7N  40341  pl42lem2N  40345  pl42lem3N  40346  pl42lem4N  40347  pl42N  40348  lhprelat3N  40405  4atex  40441  lauteq  40460  lautco  40462  ltrncoidN  40493  ltrneq2  40513  ltrnideq  40540  trlnle  40551  trlval3  40552  cdlemc  40562  cdlemd9  40571  cdlemd  40572  cdleme21j  40701  cdleme21  40702  cdleme29ex  40739  cdlemefr27cl  40768  cdlemefs27cl  40778  cdleme32d  40809  cdleme32f  40811  cdleme35h2  40822  cdleme40m  40832  cdleme17d3  40861  cdleme48fvg  40865  cdlemeg46fvcl  40871  cdlemeg46fgN  40899  cdleme48fgv  40903  cdleme50trn3  40918  cdlemb3  40971  cdlemg8  40996  cdlemg11a  41002  cdlemg15a  41020  cdlemg15  41021  cdlemg16  41022  cdlemg16z  41024  cdlemg17dN  41028  cdlemg24  41053  cdlemg37  41054  cdlemg29  41070  cdlemg33b  41072  cdlemg38  41080  cdlemg40  41082  trlco  41092  cdlemg44b  41097  ltrncom  41103  trljco  41105  tendococl  41137  tendoplcl  41146  tendoplcom  41147  cdlemj2  41187  tendoid0  41190  tendo1ne0  41193  cdlemk25-3  41269  cdlemk36  41278  cdlemkid4  41299  cdlemk19x  41308  cdlemk53  41322  cdlemk56  41336  cdleml5N  41345  tendospcanN  41388  cdlemm10N  41483  dihord6apre  41621  dihord  41629  dihmeetlem1N  41655  dihglblem2N  41659  dihmeetlem2N  41664  dihmeetbN  41668  dihmeetlem5  41673  dihmeetlem6  41674  dihmeetlem7N  41675  dihmeetlem10N  41681  dihmeetlem12N  41683  dihmeetlem16N  41687  dihmeetlem17N  41688  dihmeetlem18N  41689  dihmeetALTN  41692  dihlspsnssN  41697  dvh3dim2  41813  dvh3dim3N  41814  lcfrlem16  41923  mapdrvallem2  42010  mapdh8ad  42144  hgmapvvlem3  42290  sticksstones1  42505  sticksstones2  42506  aks6d1c6isolem1  42533  resubcan2  42747  diophrw  43105  eldioph2lem1  43106  diophrex  43121  rencldnfi  43167  pellexlem2  43176  pellqrexplicit  43223  infmrgelbi  43224  pellfundglb  43231  pellfund14gap  43233  rmxycomplete  43263  congadd  43312  acongeq  43329  jm2.19  43339  jm2.23  43342  jm2.20nn  43343  jm2.27  43354  jm3.1  43366  lnmepi  43431  lmhmlnmsplit  43433  hbtlem2  43470  dgraa0p  43495  proot1hash  43541  iocunico  43557  iocinico  43558  oasubex  43632  cantnf2  43671  onmcl  43677  omcl2  43679  nadd2rabex  43732  nadd1rabtr  43734  nadd1rabex  43736  fzunt  43800  relexpxpmin  44062  ntrclsk3  44415  grur1cld  44577  ismnu  44606  grumnudlem  44630  ismnushort  44646  rfcnnnub  45385  uzwo4  45402  wessf1ornlem  45533  supxrge  45686  infleinflem2  45718  iccintsng  45872  climsuse  45957  lptre2pt  45987  limcleqr  45991  0ellimcdiv  45996  fnlimfvre  46021  dvnprodlem1  46293  volioc  46319  stoweidlem17  46364  stoweidlem19  46366  stoweidlem20  46367  stoweidlem22  46369  stoweidlem28  46375  stoweidlem34  46381  stoweidlem44  46391  stoweidlem60  46407  wallispilem3  46414  fourierdlem42  46496  fourierdlem48  46501  fourierdlem51  46504  fourierdlem54  46507  fourierdlem74  46527  fourierdlem77  46530  fourierdlem87  46540  fourierdlem97  46550  ioorrnopnlem  46651  ovnsubaddlem2  46918  smfinflem  47164  fsupdm  47189  finfdm  47193  eluzge0nn0  47661  fzopredsuc  47672  imasetpreimafvbijlemfv  47751  lighneallem4  47959  oexpnegALTV  48026  oexpnegnz  48027  tgblthelfgott  48164  clnbgrgrim  48283  isubgr3stgrlem3  48317  rmsupp0  48717  rmsuppss  48719  lincresunit3lem3  48823  lincresunit3lem2  48829  lindssnlvec  48835  fdivmptf  48890  refdivmptf  48891  elbigolo1  48906  rrx2linest  49091  itsclc0lem1  49105  itsclc0lem2  49106  itsclc0yqsollem1  49111  itsclc0b  49121  setc1onsubc  49950