Theorem simpl2 1209

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  simpl12  1266  simpl22  1269  simpl32  1272  simp1l2  1284  simp2l2  1290  simp3l2  1296  3anandirs  1496  rspc3ev  3601  2nreu  4401  f1prex  7272  weniso  7342  ofmpteq  7687  tfisi  7843  mposn  8086  fprlem1  8285  smogt  8342  smocdmdom  8343  omeulem1  8555  nnmord  8606  nnmword  8607  naddasslem1  8669  naddasslem2  8670  difsnen  9035  enfixsn  9062  mapunen  9122  ac6sfi  9232  ordiso2  9465  wemaplem2  9497  wemapso2lem  9502  en2eqpr  9979  acndom  10023  infmap2  10188  cflim2  10235  cfsmolem  10242  coftr  10245  fin23lem26  10297  isf32lem9  10333  fin1a2lem9  10380  fin1a2lem10  10381  gchdomtri  10602  canth4  10620  gchpwdom  10643  gruima  10775  grudomon  10790  prn0  10962  distrlem4pr  10999  prlem934  11006  addcan  11382  addcan2  11383  divmulass  11883  divmulasscom  11884  ltmul1a  12055  supmul1  12175  uzsupss  12955  xaddass  13266  xleadd1a  13270  xlesubadd  13280  xmulass  13304  xlemul2a  13306  xadddilem  13311  xadddi  13312  ixxdisj  13378  ixxun  13379  ixxlb  13385  icoshftf1o  13492  icodisj  13494  ioounsn  13495  lincmb01cmp  13513  iccf1o  13514  elfz1b  13612  ssfzoulel  13780  fzoopth  13782  modmuladd  13940  modaddmulmod  13965  ltexp2a  14193  leexp2  14198  ltexp2r  14200  exple1  14204  expnlbnd2  14261  mulsubdivbinom2  14289  fun2dmnop0  14531  ccatass  14616  ccatopth  14743  pfxccatin12lem2a  14754  repswpfx  14812  repswccat  14813  cshwidxmodr  14831  2cshw  14840  repsco  14867  s2f1o  14943  limsupgle  15518  limsupgre  15522  addcn2  15635  mulcn2  15637  binomrisefac  16086  dvdsval2  16303  dvdsadd2b  16354  dvdsmod  16377  oexpneg  16393  sadass  16519  gcdass  16595  rplpwr  16606  lcmass  16662  coprmdvds2  16702  rpmulgcd2  16704  rpdvds  16708  coprmprod  16709  cncongr2  16716  rpexp  16771  prmdiveq  16835  hashgcdlem  16837  odzdvds  16845  coprimeprodsq2  16859  pythagtriplem3  16868  pythagtriplem4  16869  pcdvdsb  16919  vdwnnlem1  17045  0ram  17070  ramz2  17074  ramub1lem1  17076  mremre  17646  mrieqv2d  17685  lubss  18559  lubun  18561  clatleglb  18564  clatglbss  18565  mrelatglb  18606  isnsgrp  18771  issubmnd  18809  gsumccat  18890  frmdss2  18912  submefmnd  18944  nmzsubg  19222  ghmnsgima  19301  gsmsymgreqlem1  19491  psgnunilem4  19558  odmodnn0  19601  odnncl  19606  odmod  19607  oddvds  19608  odeq  19611  odmulgid  19615  odmulgeq  19618  odbezout  19619  odf1o1  19633  odf1o2  19634  odngen  19638  gexdvdsi  19644  pgpfi1  19656  odcau  19665  subgslw  19677  fislw  19686  lsmless1x  19705  lsmless2x  19706  lsmsubm  19714  lsmmod  19736  lsmmod2  19737  efgsfo  19800  odadd1  19909  odadd2  19910  odadd  19911  lsmcomx  19917  prdscmnd  19922  gsumconst  19995  ablsimpgfindlem1  20170  csrgbinom  20305  ring1eq0  20372  mulgass2  20383  rngisom1  20539  rhmdvdsr  20582  cntzsubrng  20643  cntzsubr  20682  isabvd  20884  rmodislmod  21020  0lmhm  21130  lmhmvsca  21135  reslmhm2b  21144  pwssplit1  21149  pwssplit2  21150  pwssplit3  21151  lbspss  21172  lspsnat  21238  lidldvgen  21462  xrsdsreclblem  21523  cssmre  21803  obs2ss  21839  uvcresum  21903  frlmsslsp  21906  frlmup4  21911  lindff1  21930  f1lindf  21932  lsslindf  21940  islindf4  21948  issubassa  21977  evlsval2  22198  coe1subfv  22387  coe1sclmul  22403  coe1sclmul2  22405  mpomatmul  22564  mamutpos  22576  scmatscmide  22625  mavmulsolcl  22669  mulmarep1gsum2  22692  mdetdiaglem  22716  mdetdiag  22717  mdetunilem1  22730  mdetunilem3  22732  mdetunilem9  22738  maducoeval2  22758  madurid  22762  slesolinvbi  22799  cramerimplem1  22801  cramerlem1  22805  cramer  22809  cpmatel2  22831  m2cpm  22859  m2pmfzmap  22865  m2cpminvid2lem  22872  m2cpminvid2  22873  decpmatmul  22890  pmatcollpw1lem2  22893  pmatcollpw1  22894  pmatcollpw2lem  22895  pmatcollpwfi  22900  pm2mpcl  22915  mply1topmatcl  22923  mp2pm2mplem2  22925  mp2pm2mplem4  22927  mp2pm2mplem5  22928  mp2pm2mp  22929  pm2mpghmlem2  22930  pm2mpghmlem1  22931  chfacfisfcpmat  22973  topssnei  23242  cnconst2  23401  cnpresti  23406  cnprest2  23408  cnpdis  23411  cnt0  23464  cnt1  23468  cnhaus  23472  sscmp  23523  hauscmp  23525  cnconn  23540  unconn  23547  finlocfin  23638  comppfsc  23650  kgen2ss  23673  ptpjopn  23730  prdstopn  23746  ptrescn  23757  qtopss  23833  kqfvima  23848  fbssint  23956  fbasrn  24002  filuni  24003  fmss  24064  rnelfm  24071  fmufil  24077  fmco  24079  flimss2  24090  flimss1  24091  flimrest  24101  cnpflf2  24118  flfcnp  24122  supnfcls  24138  fclsss1  24140  fclsss2  24141  isfcf  24152  subgntr  24225  opnsubg  24226  cldsubg  24229  ghmcnp  24233  ustuqtop1  24359  bldisj  24516  blgt0  24517  bl2in  24518  blss2ps  24521  blss2  24522  blssps  24542  blss  24543  xmetresbl  24555  lpbl  24621  blcld  24623  stdbdmopn  24636  metcnp3  24658  metcnp  24659  metcnp2  24660  txmetcnp  24665  blval2  24680  nmoix  24847  nmoi2  24848  nmotri  24857  metdsge  24968  metdseq0  24973  iocopnst  25060  xrhmeo  25066  nmhmcn  25240  cphsqrtcl2  25306  cphsqrtcl3  25307  cssbn  25495  pjth  25559  ovoliunlem2  25623  volun  25665  mbfimaopn2  25777  iblconst  25938  limcvallem  25991  dvfval  26017  dvcnp2  26040  dvcn  26041  deg1mul3le  26235  deg1tmle  26236  dvdsq1p  26281  idomrootle  26291  ig1peu  26293  ig1pdvds  26298  ply1term  26322  coeid3  26358  dgrmulc  26389  dvply1  26406  aaliou2  26462  efcvx  26570  tanord  26661  eflogeq  26725  logdivlti  26743  logccv  26786  recxpcl  26798  cxplea  26819  cxpeq  26880  ang180  26937  isosctrlem2  26942  cxp2lim  27099  amgm  27113  muval1  27255  dvdssqf  27260  mumullem2  27302  mumul  27303  bcmono  27399  lgsneg  27443  lgsdilem  27446  lgsdirprm  27453  lgsdir  27454  lgsdi  27456  lgsne0  27457  nolesgn2o  27793  nogesgn1o  27795  nosep1o  27803  nosep2o  27804  nosepssdm  27808  nosupres  27829  nosupbnd1lem1  27830  nosupbnd1lem4  27833  nosupbnd1lem5  27834  nosupbnd1lem6  27835  noinfres  27844  noinfbnd1lem1  27845  noinfbnd1lem4  27848  noinfbnd1lem6  27850  noinfbnd2  27853  noetasuplem3  27857  noetainflem3  27861  leslss  28060  cofslts  28069  coinitslts  28070  cofcutrtime  28078  addsass  28156  addsdi  28306  mulsass  28317  ltmuls2  28322  divmulsw  28344  bdayfinbndlem1  28618  z12bdaylem  28635  brbtwn2  29164  colinearalglem1  29165  colinearalg  29169  axcgrtr  29174  axsegconlem8  29183  axsegconlem9  29184  axsegconlem10  29185  axcontlem2  29224  axcontlem10  29232  elntg2  29244  ewlkle  29864  crctcshwlkn0lem5  30072  wwlknp  30101  wwlksnext  30151  wwlksnextproplem1  30167  wspthsnwspthsnon  30174  clwlkclwwlklem3  30261  erclwwlksym  30281  erclwwlknsym  30330  upgriseupth  30467  eucrct2eupth  30505  3cyclfrgrrn  30546  numclwwlk2lem1lem  30602  numclwwlk1lem2foa  30614  frgrregord13  30656  nvmul0or  30911  ipval2lem2  30965  lnoadd  31019  lnosub  31020  lnomul  31021  shless  31620  shlej1  31621  kbmul  32216  homco2  32238  kbass2  32378  eliccelico  33034  elicoelioo  33035  iocinioc2  33036  iocinif  33038  difioo  33039  nexple  33090  swrdrn2  33187  swrdrn3  33188  xrge0adddir  33251  xrge0npcan  33253  isarchi2  33418  archiabl  33431  pidlnz  33605  lindssn  33607  ssmxidl  33674  pstmfval  34203  fmcncfil  34238  zrhnm  34274  qqhnm  34297  volfiniune  34537  dya2iocnrect  34588  probinc  34728  cndprob01  34742  signswmnd  34861  bnj517  35190  cvmsss2  35637  cvmlift2lem10  35675  br6  36120  funsseq  36131  cgrtriv  36365  5segofs  36369  btwnouttr2  36385  btwnxfr  36419  lineext  36439  btwnconn1lem13  36462  brsegle2  36472  nn0prpwlem  36695  weiunpo  36838  weiunso  36839  weiunfr  36840  weiunse  36841  axtcond  36851  lindsenlbs  38126  blbnd  38298  ismtyima  38314  rrndstprj2  38342  ghomdiv  38403  grpokerinj  38404  lsatfixedN  39645  lssat  39652  lshpkrlem4  39749  cvrcon3b  39913  atlen0  39946  atcvreq0  39950  atnle  39953  atlatmstc  39955  atlatle  39956  cvlcvr1  39975  hlsupr2  40023  hlrelat2  40039  cvrexchlem  40055  lnnat  40063  atcvrj2b  40068  3dimlem3  40097  3dim1  40103  1cvrjat  40111  llni  40144  llni2  40148  llnexatN  40157  2llnmat  40160  lplni  40168  2atnelpln  40180  llncvrlpln2  40193  2llnmj  40196  lplnexatN  40199  lplnexllnN  40200  2llnm3N  40205  lvoli  40211  lvoli3  40213  lvolnle3at  40218  islvol2aN  40228  4atlem4a  40235  4atlem4b  40236  4atlem11  40245  lplncvrlvol2  40251  2lplnmj  40258  islinei  40376  linepmap  40411  lnjatN  40416  lncvrat  40418  lncmp  40419  elpaddn0  40436  elpaddatriN  40439  elpaddat  40440  paddcom  40449  paddss2  40454  paddss12  40455  paddasslem4  40459  paddasslem9  40464  paddasslem10  40465  pmodl42N  40487  pmapjoin  40488  llnmod1i2  40496  polcon2bN  40556  pclfinclN  40586  poml4N  40589  poml6N  40591  osumcllem1N  40592  osumcllem2N  40593  osumcllem11N  40602  osumclN  40603  pmapojoinN  40604  pexmidlem2N  40607  pexmidlem3N  40608  pexmidlem4N  40609  pexmidlem6N  40611  pexmidlem7N  40612  pl42lem2N  40616  pl42lem3N  40617  pl42lem4N  40618  pl42N  40619  lhprelat3N  40676  4atex  40712  lauteq  40731  lautco  40733  ltrncoidN  40764  ltrneq2  40784  ltrnideq  40811  trlnle  40822  trlval3  40823  cdlemc  40833  cdlemd9  40842  cdlemd  40843  cdleme21j  40972  cdleme21  40973  cdleme29ex  41010  cdlemefr27cl  41039  cdlemefs27cl  41049  cdleme32d  41080  cdleme32f  41082  cdleme35h2  41093  cdleme40m  41103  cdleme17d3  41132  cdleme48fvg  41136  cdlemeg46fvcl  41142  cdlemeg46fgN  41170  cdleme48fgv  41174  cdleme50trn3  41189  cdlemb3  41242  cdlemg8  41267  cdlemg11a  41273  cdlemg15a  41291  cdlemg15  41292  cdlemg16  41293  cdlemg16z  41295  cdlemg17dN  41299  cdlemg24  41324  cdlemg37  41325  cdlemg29  41341  cdlemg33b  41343  cdlemg38  41351  cdlemg40  41353  trlco  41363  cdlemg44b  41368  ltrncom  41374  trljco  41376  tendococl  41408  tendoplcl  41417  tendoplcom  41418  cdlemj2  41458  tendoid0  41461  tendo1ne0  41464  cdlemk25-3  41540  cdlemk36  41549  cdlemkid4  41570  cdlemk19x  41579  cdlemk53  41593  cdlemk56  41607  cdleml5N  41616  tendospcanN  41659  cdlemm10N  41754  dihord6apre  41892  dihord  41900  dihmeetlem1N  41926  dihglblem2N  41930  dihmeetlem2N  41935  dihmeetbN  41939  dihmeetlem5  41944  dihmeetlem6  41945  dihmeetlem7N  41946  dihmeetlem10N  41952  dihmeetlem12N  41954  dihmeetlem16N  41958  dihmeetlem17N  41959  dihmeetlem18N  41960  dihmeetALTN  41963  dihlspsnssN  41968  dvh3dim2  42084  dvh3dim3N  42085  lcfrlem16  42194  mapdrvallem2  42281  mapdh8ad  42415  hgmapvvlem3  42561  sticksstones1  42775  sticksstones2  42776  aks6d1c6isolem1  42803  resubcan2  43009  diophrw  43352  eldioph2lem1  43353  diophrex  43368  rencldnfi  43410  pellexlem2  43419  pellqrexplicit  43466  infmrgelbi  43467  pellfundglb  43474  pellfund14gap  43476  rmxycomplete  43506  congadd  43555  acongeq  43572  jm2.19  43582  jm2.23  43585  jm2.20nn  43586  jm2.27  43597  jm3.1  43609  lnmepi  43674  lmhmlnmsplit  43676  hbtlem2  43713  dgraa0p  43738  proot1hash  43784  iocunico  43800  iocinico  43801  oasubex  43875  cantnf2  43914  onmcl  43920  omcl2  43922  nadd2rabex  43975  nadd1rabtr  43977  nadd1rabex  43979  fzunt  44043  relexpxpmin  44305  ntrclsk3  44658  grur1cld  44820  ismnu  44835  grumnudlem  44859  ismnushort  44875  rfcnnnub  45614  uzwo4  45631  wessf1ornlem  45761  supxrge  45912  infleinflem2  45944  iccintsng  46097  climsuse  46182  lptre2pt  46212  limcleqr  46216  0ellimcdiv  46221  fnlimfvre  46246  dvnprodlem1  46518  volioc  46544  stoweidlem17  46589  stoweidlem19  46591  stoweidlem20  46592  stoweidlem22  46594  stoweidlem28  46600  stoweidlem34  46606  stoweidlem44  46616  stoweidlem60  46632  wallispilem3  46639  fourierdlem42  46721  fourierdlem48  46726  fourierdlem51  46729  fourierdlem54  46732  fourierdlem74  46752  fourierdlem77  46755  fourierdlem87  46765  fourierdlem97  46775  ioorrnopnlem  46876  ovnsubaddlem2  47143  smfinflem  47389  fsupdm  47414  finfdm  47418  eluzge0nn0  47904  fzopredsuc  47916  imasetpreimafvbijlemfv  48006  lighneallem4  48217  oexpnegALTV  48297  oexpnegnz  48298  tgblthelfgott  48435  clnbgrgrim  48554  isubgr3stgrlem3  48588  rmsupp0  48999  rmsuppss  49001  lincresunit3lem3  49105  lincresunit3lem2  49111  lindssnlvec  49117  fdivmptf  49172  refdivmptf  49173  elbigolo1  49188  rrx2linest  49373  itsclc0lem1  49387  itsclc0lem2  49388  itsclc0yqsollem1  49393  itsclc0b  49403  setc1onsubc  50231