Theorem simpl2 1193

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

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

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 1088

This theorem is referenced by:  simpl12  1250  simpl22  1253  simpl32  1256  simp1l2  1268  simp2l2  1274  simp3l2  1280  3anandirs  1474  rspc3ev  3591  2nreu  4395  f1prex  7227  weniso  7297  ofmpteq  7642  tfisi  7798  mposn  8042  fprlem1  8239  smogt  8296  smocdmdom  8297  omeulem1  8506  nnmord  8556  nnmword  8557  naddasslem1  8618  naddasslem2  8619  difsnen  8982  enfixsn  9009  mapunen  9069  ac6sfi  9178  ordiso2  9411  wemaplem2  9443  wemapso2lem  9448  en2eqpr  9908  acndom  9952  infmap2  10118  cflim2  10164  cfsmolem  10171  coftr  10174  fin23lem26  10226  isf32lem9  10262  fin1a2lem9  10309  fin1a2lem10  10310  gchdomtri  10530  canth4  10548  gchpwdom  10571  gruima  10703  grudomon  10718  prn0  10890  distrlem4pr  10927  prlem934  10934  addcan  11307  addcan2  11308  divmulass  11809  divmulasscom  11810  ltmul1a  11980  supmul1  12101  uzsupss  12848  xaddass  13158  xleadd1a  13162  xlesubadd  13172  xmulass  13196  xlemul2a  13198  xadddilem  13203  xadddi  13204  ixxdisj  13270  ixxun  13271  ixxlb  13277  icoshftf1o  13384  icodisj  13386  ioounsn  13387  lincmb01cmp  13405  iccf1o  13406  elfz1b  13503  ssfzoulel  13670  fzoopth  13672  modmuladd  13830  modaddmulmod  13855  ltexp2a  14083  leexp2  14088  ltexp2r  14090  exple1  14094  expnlbnd2  14151  mulsubdivbinom2  14179  fun2dmnop0  14421  ccatass  14506  ccatopth  14633  pfxccatin12lem2a  14644  repswpfx  14702  repswccat  14703  cshwidxmodr  14721  2cshw  14730  repsco  14757  s2f1o  14833  limsupgle  15394  limsupgre  15398  addcn2  15511  mulcn2  15513  binomrisefac  15959  dvdsval2  16176  dvdsadd2b  16227  dvdsmod  16250  oexpneg  16266  sadass  16392  gcdass  16468  rplpwr  16479  lcmass  16535  coprmdvds2  16575  rpmulgcd2  16577  rpdvds  16581  coprmprod  16582  cncongr2  16589  rpexp  16643  prmdiveq  16707  hashgcdlem  16709  odzdvds  16717  coprimeprodsq2  16731  pythagtriplem3  16740  pythagtriplem4  16741  pcdvdsb  16791  vdwnnlem1  16917  0ram  16942  ramz2  16946  ramub1lem1  16948  mremre  17516  mrieqv2d  17555  lubss  18429  lubun  18431  clatleglb  18434  clatglbss  18435  mrelatglb  18476  isnsgrp  18641  issubmnd  18679  gsumccat  18759  frmdss2  18781  submefmnd  18813  nmzsubg  19087  ghmnsgima  19162  gsmsymgreqlem1  19352  psgnunilem4  19419  odmodnn0  19462  odnncl  19467  odmod  19468  oddvds  19469  odeq  19472  odmulgid  19476  odmulgeq  19479  odbezout  19480  odf1o1  19494  odf1o2  19495  odngen  19499  gexdvdsi  19505  pgpfi1  19517  odcau  19526  subgslw  19538  fislw  19547  lsmless1x  19566  lsmless2x  19567  lsmsubm  19575  lsmmod  19597  lsmmod2  19598  efgsfo  19661  odadd1  19770  odadd2  19771  odadd  19772  lsmcomx  19778  prdscmnd  19783  gsumconst  19856  ablsimpgfindlem1  20031  srg1zr  20143  csrgbinom  20160  ring1eq0  20226  mulgass2  20237  rngisom1  20394  rhmdvdsr  20433  cntzsubrng  20492  cntzsubr  20531  isabvd  20737  rmodislmod  20873  0lmhm  20984  lmhmvsca  20989  reslmhm2b  20998  pwssplit1  21003  pwssplit2  21004  pwssplit3  21005  lbspss  21026  lspsnat  21092  lidldvgen  21281  xrsdsreclblem  21359  cssmre  21640  obs2ss  21676  uvcresum  21740  frlmsslsp  21743  frlmup4  21748  lindff1  21767  f1lindf  21769  lsslindf  21777  islindf4  21785  issubassa  21814  evlsval2  22032  coe1subfv  22190  coe1sclmul  22206  coe1sclmul2  22208  mpomatmul  22371  mamutpos  22383  scmatscmide  22432  mavmulsolcl  22476  mulmarep1gsum2  22499  mdetdiaglem  22523  mdetdiag  22524  mdetunilem1  22537  mdetunilem3  22539  mdetunilem9  22545  maducoeval2  22565  madurid  22569  slesolinvbi  22606  cramerimplem1  22608  cramerlem1  22612  cramer  22616  cpmatel2  22638  m2cpm  22666  m2pmfzmap  22672  m2cpminvid2lem  22679  m2cpminvid2  22680  decpmatmul  22697  pmatcollpw1lem2  22700  pmatcollpw1  22701  pmatcollpw2lem  22702  pmatcollpwfi  22707  pm2mpcl  22722  mply1topmatcl  22730  mp2pm2mplem2  22732  mp2pm2mplem4  22734  mp2pm2mplem5  22735  mp2pm2mp  22736  pm2mpghmlem2  22737  pm2mpghmlem1  22738  chfacfisfcpmat  22780  topssnei  23049  cnconst2  23208  cnpresti  23213  cnprest2  23215  cnpdis  23218  cnt0  23271  cnt1  23275  cnhaus  23279  sscmp  23330  hauscmp  23332  cnconn  23347  unconn  23354  finlocfin  23445  comppfsc  23457  kgen2ss  23480  ptpjopn  23537  prdstopn  23553  ptrescn  23564  qtopss  23640  kqfvima  23655  fbssint  23763  fbasrn  23809  filuni  23810  fmss  23871  rnelfm  23878  fmufil  23884  fmco  23886  flimss2  23897  flimss1  23898  flimrest  23908  cnpflf2  23925  flfcnp  23929  supnfcls  23945  fclsss1  23947  fclsss2  23948  isfcf  23959  subgntr  24032  opnsubg  24033  cldsubg  24036  ghmcnp  24040  ustuqtop1  24166  bldisj  24323  blgt0  24324  bl2in  24325  blss2ps  24328  blss2  24329  blssps  24349  blss  24350  xmetresbl  24362  lpbl  24428  blcld  24430  stdbdmopn  24443  metcnp3  24465  metcnp  24466  metcnp2  24467  txmetcnp  24472  blval2  24487  nmoix  24654  nmoi2  24655  nmotri  24664  metdsge  24775  metdseq0  24780  iocopnst  24874  xrhmeo  24881  nmhmcn  25057  cphsqrtcl2  25123  cphsqrtcl3  25124  cssbn  25312  pjth  25376  ovoliunlem2  25441  volun  25483  mbfimaopn2  25595  iblconst  25756  limcvallem  25809  dvfval  25835  dvcnp2  25858  dvcnp2OLD  25859  dvcn  25860  deg1mul3le  26059  deg1tmle  26060  dvdsq1p  26105  idomrootle  26115  ig1peu  26117  ig1pdvds  26122  ply1term  26146  coeid3  26182  dgrmulc  26214  dvply1  26228  aaliou2  26285  efcvx  26396  tanord  26484  eflogeq  26548  logdivlti  26566  logccv  26609  recxpcl  26621  cxplea  26642  cxpeq  26704  ang180  26761  isosctrlem2  26766  cxp2lim  26924  amgm  26938  muval1  27080  dvdssqf  27085  mumullem2  27127  mumul  27128  bcmono  27225  lgsneg  27269  lgsdilem  27272  lgsdirprm  27279  lgsdir  27280  lgsdi  27282  lgsne0  27283  nolesgn2o  27620  nogesgn1o  27622  nosep1o  27630  nosep2o  27631  nosepssdm  27635  nosupres  27656  nosupbnd1lem1  27657  nosupbnd1lem4  27660  nosupbnd1lem5  27661  nosupbnd1lem6  27662  noinfres  27671  noinfbnd1lem1  27672  noinfbnd1lem4  27675  noinfbnd1lem6  27677  noinfbnd2  27680  noetasuplem3  27684  noetainflem3  27688  slelss  27864  cofsslt  27872  coinitsslt  27873  cofcutrtime  27881  addsass  27958  addsdi  28104  mulsass  28115  sltmul2  28120  divsmulw  28142  brbtwn2  28894  colinearalglem1  28895  colinearalg  28899  axcgrtr  28904  axsegconlem8  28913  axsegconlem9  28914  axsegconlem10  28915  axcontlem2  28954  axcontlem10  28962  elntg2  28974  ewlkle  29595  crctcshwlkn0lem5  29803  wwlknp  29832  wwlksnext  29882  wwlksnextproplem1  29898  wspthsnwspthsnon  29905  clwlkclwwlklem3  29992  erclwwlksym  30012  erclwwlknsym  30061  upgriseupth  30198  eucrct2eupth  30236  3cyclfrgrrn  30277  numclwwlk2lem1lem  30333  numclwwlk1lem2foa  30345  frgrregord13  30387  nvmul0or  30641  ipval2lem2  30695  lnoadd  30749  lnosub  30750  lnomul  30751  shless  31350  shlej1  31351  kbmul  31946  homco2  31968  kbass2  32108  eliccelico  32771  elicoelioo  32772  iocinioc2  32773  iocinif  32775  difioo  32776  nexple  32838  swrdrn2  32946  swrdrn3  32947  xrge0adddir  33010  xrge0npcan  33012  isarchi2  33165  archiabl  33178  pidlnz  33352  lindssn  33354  ssmxidl  33450  pstmfval  33920  fmcncfil  33955  zrhnm  33991  qqhnm  34014  volfiniune  34254  dya2iocnrect  34305  probinc  34445  cndprob01  34459  signswmnd  34581  bnj517  34908  cvmsss2  35329  cvmlift2lem10  35367  br6  35812  funsseq  35823  cgrtriv  36057  5segofs  36061  btwnouttr2  36077  btwnxfr  36111  lineext  36131  btwnconn1lem13  36154  brsegle2  36164  nn0prpwlem  36377  weiunpo  36520  weiunso  36521  weiunfr  36522  weiunse  36523  lindsenlbs  37665  blbnd  37837  ismtyima  37853  rrndstprj2  37881  ghomdiv  37942  grpokerinj  37943  lsatfixedN  39118  lssat  39125  lshpkrlem4  39222  cvrcon3b  39386  atlen0  39419  atcvreq0  39423  atnle  39426  atlatmstc  39428  atlatle  39429  cvlcvr1  39448  hlsupr2  39496  hlrelat2  39512  cvrexchlem  39528  lnnat  39536  atcvrj2b  39541  3dimlem3  39570  3dim1  39576  1cvrjat  39584  llni  39617  llni2  39621  llnexatN  39630  2llnmat  39633  lplni  39641  2atnelpln  39653  llncvrlpln2  39666  2llnmj  39669  lplnexatN  39672  lplnexllnN  39673  2llnm3N  39678  lvoli  39684  lvoli3  39686  lvolnle3at  39691  islvol2aN  39701  4atlem4a  39708  4atlem4b  39709  4atlem11  39718  lplncvrlvol2  39724  2lplnmj  39731  islinei  39849  linepmap  39884  lnjatN  39889  lncvrat  39891  lncmp  39892  elpaddn0  39909  elpaddatriN  39912  elpaddat  39913  paddcom  39922  paddss2  39927  paddss12  39928  paddasslem4  39932  paddasslem9  39937  paddasslem10  39938  pmodl42N  39960  pmapjoin  39961  llnmod1i2  39969  polcon2bN  40029  pclfinclN  40059  poml4N  40062  poml6N  40064  osumcllem1N  40065  osumcllem2N  40066  osumcllem11N  40075  osumclN  40076  pmapojoinN  40077  pexmidlem2N  40080  pexmidlem3N  40081  pexmidlem4N  40082  pexmidlem6N  40084  pexmidlem7N  40085  pl42lem2N  40089  pl42lem3N  40090  pl42lem4N  40091  pl42N  40092  lhprelat3N  40149  4atex  40185  lauteq  40204  lautco  40206  ltrncoidN  40237  ltrneq2  40257  ltrnideq  40284  trlnle  40295  trlval3  40296  cdlemc  40306  cdlemd9  40315  cdlemd  40316  cdleme21j  40445  cdleme21  40446  cdleme29ex  40483  cdlemefr27cl  40512  cdlemefs27cl  40522  cdleme32d  40553  cdleme32f  40555  cdleme35h2  40566  cdleme40m  40576  cdleme17d3  40605  cdleme48fvg  40609  cdlemeg46fvcl  40615  cdlemeg46fgN  40643  cdleme48fgv  40647  cdleme50trn3  40662  cdlemb3  40715  cdlemg8  40740  cdlemg11a  40746  cdlemg15a  40764  cdlemg15  40765  cdlemg16  40766  cdlemg16z  40768  cdlemg17dN  40772  cdlemg24  40797  cdlemg37  40798  cdlemg29  40814  cdlemg33b  40816  cdlemg38  40824  cdlemg40  40826  trlco  40836  cdlemg44b  40841  ltrncom  40847  trljco  40849  tendococl  40881  tendoplcl  40890  tendoplcom  40891  cdlemj2  40931  tendoid0  40934  tendo1ne0  40937  cdlemk25-3  41013  cdlemk36  41022  cdlemkid4  41043  cdlemk19x  41052  cdlemk53  41066  cdlemk56  41080  cdleml5N  41089  tendospcanN  41132  cdlemm10N  41227  dihord6apre  41365  dihord  41373  dihmeetlem1N  41399  dihglblem2N  41403  dihmeetlem2N  41408  dihmeetbN  41412  dihmeetlem5  41417  dihmeetlem6  41418  dihmeetlem7N  41419  dihmeetlem10N  41425  dihmeetlem12N  41427  dihmeetlem16N  41431  dihmeetlem17N  41432  dihmeetlem18N  41433  dihmeetALTN  41436  dihlspsnssN  41441  dvh3dim2  41557  dvh3dim3N  41558  lcfrlem16  41667  mapdrvallem2  41754  mapdh8ad  41888  hgmapvvlem3  42034  sticksstones1  42249  sticksstones2  42250  aks6d1c6isolem1  42277  resubcan2  42496  diophrw  42866  eldioph2lem1  42867  diophrex  42882  rencldnfi  42928  pellexlem2  42937  pellqrexplicit  42984  infmrgelbi  42985  pellfundglb  42992  pellfund14gap  42994  rmxycomplete  43024  congadd  43073  acongeq  43090  jm2.19  43100  jm2.23  43103  jm2.20nn  43104  jm2.27  43115  jm3.1  43127  lnmepi  43192  lmhmlnmsplit  43194  hbtlem2  43231  dgraa0p  43256  proot1hash  43302  iocunico  43318  iocinico  43319  oasubex  43393  cantnf2  43432  onmcl  43438  omcl2  43440  nadd2rabex  43493  nadd1rabtr  43495  nadd1rabex  43497  fzunt  43562  relexpxpmin  43824  ntrclsk3  44177  grur1cld  44339  ismnu  44368  grumnudlem  44392  ismnushort  44408  rfcnnnub  45147  uzwo4  45164  wessf1ornlem  45296  supxrge  45451  infleinflem2  45483  iccintsng  45637  climsuse  45722  lptre2pt  45752  limcleqr  45756  0ellimcdiv  45761  fnlimfvre  45786  dvnprodlem1  46058  volioc  46084  stoweidlem17  46129  stoweidlem19  46131  stoweidlem20  46132  stoweidlem22  46134  stoweidlem28  46140  stoweidlem34  46146  stoweidlem44  46156  stoweidlem60  46172  wallispilem3  46179  fourierdlem42  46261  fourierdlem48  46266  fourierdlem51  46269  fourierdlem54  46272  fourierdlem74  46292  fourierdlem77  46295  fourierdlem87  46305  fourierdlem97  46315  ioorrnopnlem  46416  ovnsubaddlem2  46683  smfinflem  46929  fsupdm  46954  finfdm  46958  eluzge0nn0  47426  fzopredsuc  47437  imasetpreimafvbijlemfv  47516  lighneallem4  47724  oexpnegALTV  47791  oexpnegnz  47792  tgblthelfgott  47929  clnbgrgrim  48048  isubgr3stgrlem3  48082  rmsupp0  48482  rmsuppss  48484  lincresunit3lem3  48589  lincresunit3lem2  48595  lindssnlvec  48601  fdivmptf  48656  refdivmptf  48657  elbigolo1  48672  rrx2linest  48857  itsclc0lem1  48871  itsclc0lem2  48872  itsclc0yqsollem1  48877  itsclc0b  48887  setc1onsubc  49717