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  3626  2nreu  4442  f1prex  7293  weniso  7362  ofmpteq  7707  tfisi  7863  mposn  8108  fprlem1  8306  smogt  8388  smocdmdom  8389  omeulem1  8603  nnmord  8653  nnmword  8654  naddasslem1  8715  naddasslem2  8716  difsnen  9078  enfixsn  9106  mapunen  9171  ac6sfi  9312  ordiso2  9539  wemaplem2  9571  wemapso2lem  9576  en2eqpr  10031  acndom  10075  infmap2  10242  cflim2  10287  cfsmolem  10294  coftr  10297  fin23lem26  10349  isf32lem9  10385  fin1a2lem9  10432  fin1a2lem10  10433  gchdomtri  10653  canth4  10671  gchpwdom  10694  gruima  10826  grudomon  10841  prn0  11013  distrlem4pr  11050  prlem934  11057  addcan  11429  addcan2  11430  divmulass  11926  divmulasscom  11927  ltmul1a  12094  supmul1  12214  uzsupss  12955  xaddass  13261  xleadd1a  13265  xlesubadd  13275  xmulass  13299  xlemul2a  13301  xadddilem  13306  xadddi  13307  ixxdisj  13372  ixxun  13373  ixxlb  13379  icoshftf1o  13484  icodisj  13486  ioounsn  13487  lincmb01cmp  13505  iccf1o  13506  elfz1b  13603  ssfzoulel  13759  modmuladd  13911  modaddmulmod  13936  ltexp2a  14163  leexp2  14168  ltexp2r  14170  exple1  14173  expnlbnd2  14229  mulsubdivbinom2  14254  fun2dmnop0  14488  ccatass  14571  ccatopth  14699  pfxccatin12lem2a  14710  repswpfx  14768  repswccat  14769  cshwidxmodr  14787  2cshw  14796  repsco  14824  s2f1o  14900  limsupgle  15454  limsupgre  15458  addcn2  15571  mulcn2  15573  binomrisefac  16019  dvdsval2  16234  dvdsadd2b  16283  dvdsmod  16306  oexpneg  16322  sadass  16446  gcdass  16523  rplpwr  16533  lcmass  16585  coprmdvds2  16625  rpmulgcd2  16627  rpdvds  16631  coprmprod  16632  cncongr2  16639  rpexp  16694  prmdiveq  16755  hashgcdlem  16757  odzdvds  16764  coprimeprodsq2  16778  pythagtriplem3  16787  pythagtriplem4  16788  pcdvdsb  16838  vdwnnlem1  16964  0ram  16989  ramz2  16993  ramub1lem1  16995  mremre  17584  mrieqv2d  17619  lubss  18505  lubun  18507  clatleglb  18510  clatglbss  18511  mrelatglb  18552  isnsgrp  18683  issubmnd  18721  gsumccat  18793  frmdss2  18815  submefmnd  18847  nmzsubg  19120  ghmnsgima  19194  gsmsymgreqlem1  19385  psgnunilem4  19452  odmodnn0  19495  odnncl  19500  odmod  19501  oddvds  19502  odeq  19505  odmulgid  19509  odmulgeq  19512  odbezout  19513  odf1o1  19527  odf1o2  19528  odngen  19532  gexdvdsi  19538  pgpfi1  19550  odcau  19559  subgslw  19571  fislw  19580  lsmless1x  19599  lsmless2x  19600  lsmsubm  19608  lsmmod  19630  lsmmod2  19631  efgsfo  19694  odadd1  19803  odadd2  19804  odadd  19805  lsmcomx  19811  prdscmnd  19816  gsumconst  19889  ablsimpgfindlem1  20064  srg1zr  20155  csrgbinom  20172  ring1eq0  20234  mulgass2  20245  rngisom1  20405  rhmdvdsr  20447  cntzsubrng  20504  cntzsubr  20545  isabvd  20700  rmodislmod  20813  rmodislmodOLD  20814  0lmhm  20925  lmhmvsca  20930  reslmhm2b  20939  pwssplit1  20944  pwssplit2  20945  pwssplit3  20946  lbspss  20967  lspsnat  21033  lidldvgen  21224  xrsdsreclblem  21345  cssmre  21625  obs2ss  21663  uvcresum  21727  frlmsslsp  21730  frlmup4  21735  lindff1  21754  f1lindf  21756  lsslindf  21764  islindf4  21772  issubassa  21800  evlsval2  22033  coe1subfv  22185  coe1sclmul  22201  coe1sclmul2  22203  mpomatmul  22361  mamutpos  22373  scmatscmide  22422  mavmulsolcl  22466  mulmarep1gsum2  22489  mdetdiaglem  22513  mdetdiag  22514  mdetunilem1  22527  mdetunilem3  22529  mdetunilem9  22535  maducoeval2  22555  madurid  22559  slesolinvbi  22596  cramerimplem1  22598  cramerlem1  22602  cramer  22606  cpmatel2  22628  m2cpm  22656  m2pmfzmap  22662  m2cpminvid2lem  22669  m2cpminvid2  22670  decpmatmul  22687  pmatcollpw1lem2  22690  pmatcollpw1  22691  pmatcollpw2lem  22692  pmatcollpwfi  22697  pm2mpcl  22712  mply1topmatcl  22720  mp2pm2mplem2  22722  mp2pm2mplem4  22724  mp2pm2mplem5  22725  mp2pm2mp  22726  pm2mpghmlem2  22727  pm2mpghmlem1  22728  chfacfisfcpmat  22770  topssnei  23041  cnconst2  23200  cnpresti  23205  cnprest2  23207  cnpdis  23210  cnt0  23263  cnt1  23267  cnhaus  23271  sscmp  23322  hauscmp  23324  cnconn  23339  unconn  23346  finlocfin  23437  comppfsc  23449  kgen2ss  23472  ptpjopn  23529  prdstopn  23545  ptrescn  23556  qtopss  23632  kqfvima  23647  fbssint  23755  fbasrn  23801  filuni  23802  fmss  23863  rnelfm  23870  fmufil  23876  fmco  23878  flimss2  23889  flimss1  23890  flimrest  23900  cnpflf2  23917  flfcnp  23921  supnfcls  23937  fclsss1  23939  fclsss2  23940  isfcf  23951  subgntr  24024  opnsubg  24025  cldsubg  24028  ghmcnp  24032  ustuqtop1  24159  bldisj  24317  blgt0  24318  bl2in  24319  blss2ps  24322  blss2  24323  blssps  24343  blss  24344  xmetresbl  24356  lpbl  24425  blcld  24427  stdbdmopn  24440  metcnp3  24462  metcnp  24463  metcnp2  24464  txmetcnp  24469  blval2  24484  nmoix  24659  nmoi2  24660  nmotri  24669  metdsge  24778  metdseq0  24783  iocopnst  24877  xrhmeo  24884  nmhmcn  25060  cphsqrtcl2  25127  cphsqrtcl3  25128  cssbn  25316  pjth  25380  ovoliunlem2  25445  volun  25487  mbfimaopn2  25599  iblconst  25760  limcvallem  25813  dvfval  25839  dvcnp2  25862  dvcnp2OLD  25863  dvcn  25864  deg1mul3le  26065  deg1tmle  26066  dvdsq1p  26110  idomrootle  26120  ig1peu  26122  ig1pdvds  26127  ply1term  26151  coeid3  26187  dgrmulc  26219  dvply1  26231  aaliou2  26288  efcvx  26399  tanord  26485  eflogeq  26549  logdivlti  26567  logccv  26610  recxpcl  26622  cxplea  26643  cxpeq  26705  ang180  26759  isosctrlem2  26764  cxp2lim  26922  amgm  26936  muval1  27078  dvdssqf  27083  mumullem2  27125  mumul  27126  bcmono  27223  lgsneg  27267  lgsdilem  27270  lgsdirprm  27277  lgsdir  27278  lgsdi  27280  lgsne0  27281  nolesgn2o  27617  nogesgn1o  27619  nosep1o  27627  nosep2o  27628  nosepssdm  27632  nosupres  27653  nosupbnd1lem1  27654  nosupbnd1lem4  27657  nosupbnd1lem5  27658  nosupbnd1lem6  27659  noinfres  27668  noinfbnd1lem1  27669  noinfbnd1lem4  27672  noinfbnd1lem6  27674  noinfbnd2  27677  noetasuplem3  27681  noetainflem3  27685  slelss  27847  cofsslt  27851  coinitsslt  27852  cofcutrtime  27860  addsass  27935  addsdi  28068  mulsass  28079  sltmul2  28084  divsmulw  28105  brbtwn2  28729  colinearalglem1  28730  colinearalg  28734  axcgrtr  28739  axsegconlem8  28748  axsegconlem9  28749  axsegconlem10  28750  axcontlem2  28789  axcontlem10  28797  elntg2  28809  ewlkle  29432  crctcshwlkn0lem5  29638  wwlknp  29667  wwlksnext  29717  wwlksnextproplem1  29733  wspthsnwspthsnon  29740  clwlkclwwlklem3  29824  erclwwlksym  29844  erclwwlknsym  29893  upgriseupth  30030  eucrct2eupth  30068  3cyclfrgrrn  30109  numclwwlk2lem1lem  30165  numclwwlk1lem2foa  30177  frgrregord13  30219  nvmul0or  30473  ipval2lem2  30527  lnoadd  30581  lnosub  30582  lnomul  30583  shless  31182  shlej1  31183  kbmul  31778  homco2  31800  kbass2  31940  eliccelico  32558  elicoelioo  32559  iocinioc2  32560  iocinif  32562  difioo  32563  swrdrn2  32688  swrdrn3  32689  xrge0adddir  32761  xrge0npcan  32763  isarchi2  32906  archiabl  32919  pidlnz  33100  lindssn  33106  ssmxidl  33200  pstmfval  33497  fmcncfil  33532  zrhnm  33570  qqhnm  33591  nexple  33628  volfiniune  33849  dya2iocnrect  33901  probinc  34041  cndprob01  34055  signswmnd  34189  bnj517  34516  cvmsss2  34884  cvmlift2lem10  34922  br6  35351  funsseq  35363  cgrtriv  35598  5segofs  35602  btwnouttr2  35618  btwnxfr  35652  lineext  35672  btwnconn1lem13  35695  brsegle2  35705  nn0prpwlem  35806  lindsenlbs  37088  blbnd  37260  ismtyima  37276  rrndstprj2  37304  ghomdiv  37365  grpokerinj  37366  lsatfixedN  38481  lssat  38488  lshpkrlem4  38585  cvrcon3b  38749  atlen0  38782  atcvreq0  38786  atnle  38789  atlatmstc  38791  atlatle  38792  cvlcvr1  38811  hlsupr2  38860  hlrelat2  38876  cvrexchlem  38892  lnnat  38900  atcvrj2b  38905  3dimlem3  38934  3dim1  38940  1cvrjat  38948  llni  38981  llni2  38985  llnexatN  38994  2llnmat  38997  lplni  39005  2atnelpln  39017  llncvrlpln2  39030  2llnmj  39033  lplnexatN  39036  lplnexllnN  39037  2llnm3N  39042  lvoli  39048  lvoli3  39050  lvolnle3at  39055  islvol2aN  39065  4atlem4a  39072  4atlem4b  39073  4atlem11  39082  lplncvrlvol2  39088  2lplnmj  39095  islinei  39213  linepmap  39248  lnjatN  39253  lncvrat  39255  lncmp  39256  elpaddn0  39273  elpaddatriN  39276  elpaddat  39277  paddcom  39286  paddss2  39291  paddss12  39292  paddasslem4  39296  paddasslem9  39301  paddasslem10  39302  pmodl42N  39324  pmapjoin  39325  llnmod1i2  39333  polcon2bN  39393  pclfinclN  39423  poml4N  39426  poml6N  39428  osumcllem1N  39429  osumcllem2N  39430  osumcllem11N  39439  osumclN  39440  pmapojoinN  39441  pexmidlem2N  39444  pexmidlem3N  39445  pexmidlem4N  39446  pexmidlem6N  39448  pexmidlem7N  39449  pl42lem2N  39453  pl42lem3N  39454  pl42lem4N  39455  pl42N  39456  lhprelat3N  39513  4atex  39549  lauteq  39568  lautco  39570  ltrncoidN  39601  ltrneq2  39621  ltrnideq  39648  trlnle  39659  trlval3  39660  cdlemc  39670  cdlemd9  39679  cdlemd  39680  cdleme21j  39809  cdleme21  39810  cdleme29ex  39847  cdlemefr27cl  39876  cdlemefs27cl  39886  cdleme32d  39917  cdleme32f  39919  cdleme35h2  39930  cdleme40m  39940  cdleme17d3  39969  cdleme48fvg  39973  cdlemeg46fvcl  39979  cdlemeg46fgN  40007  cdleme48fgv  40011  cdleme50trn3  40026  cdlemb3  40079  cdlemg8  40104  cdlemg11a  40110  cdlemg15a  40128  cdlemg15  40129  cdlemg16  40130  cdlemg16z  40132  cdlemg17dN  40136  cdlemg24  40161  cdlemg37  40162  cdlemg29  40178  cdlemg33b  40180  cdlemg38  40188  cdlemg40  40190  trlco  40200  cdlemg44b  40205  ltrncom  40211  trljco  40213  tendococl  40245  tendoplcl  40254  tendoplcom  40255  cdlemj2  40295  tendoid0  40298  tendo1ne0  40301  cdlemk25-3  40377  cdlemk36  40386  cdlemkid4  40407  cdlemk19x  40416  cdlemk53  40430  cdlemk56  40444  cdleml5N  40453  tendospcanN  40496  cdlemm10N  40591  dihord6apre  40729  dihord  40737  dihmeetlem1N  40763  dihglblem2N  40767  dihmeetlem2N  40772  dihmeetbN  40776  dihmeetlem5  40781  dihmeetlem6  40782  dihmeetlem7N  40783  dihmeetlem10N  40789  dihmeetlem12N  40791  dihmeetlem16N  40795  dihmeetlem17N  40796  dihmeetlem18N  40797  dihmeetALTN  40800  dihlspsnssN  40805  dvh3dim2  40921  dvh3dim3N  40922  lcfrlem16  41031  mapdrvallem2  41118  mapdh8ad  41252  hgmapvvlem3  41398  sticksstones1  41618  sticksstones2  41619  aks6d1c6isolem1  41646  resubcan2  41943  diophrw  42179  eldioph2lem1  42180  diophrex  42195  rencldnfi  42241  pellexlem2  42250  pellqrexplicit  42297  infmrgelbi  42298  pellfundglb  42305  pellfund14gap  42307  rmxycomplete  42338  congadd  42387  acongeq  42404  jm2.19  42414  jm2.23  42417  jm2.20nn  42418  jm2.27  42429  jm3.1  42441  lnmepi  42509  lmhmlnmsplit  42511  hbtlem2  42548  dgraa0p  42573  proot1hash  42623  iocunico  42639  iocinico  42640  oasubex  42715  cantnf2  42754  onmcl  42760  omcl2  42762  nadd2rabex  42815  nadd1rabtr  42817  nadd1rabex  42819  fzunt  42885  relexpxpmin  43147  ntrclsk3  43500  grur1cld  43669  ismnu  43698  grumnudlem  43722  ismnushort  43738  rfcnnnub  44398  uzwo4  44417  wessf1ornlem  44558  supxrge  44720  infleinflem2  44753  iccintsng  44908  climsuse  44996  lptre2pt  45028  limcleqr  45032  0ellimcdiv  45037  fnlimfvre  45062  dvnprodlem1  45334  volioc  45360  stoweidlem17  45405  stoweidlem19  45407  stoweidlem20  45408  stoweidlem22  45410  stoweidlem28  45416  stoweidlem34  45422  stoweidlem44  45432  stoweidlem60  45448  wallispilem3  45455  fourierdlem42  45537  fourierdlem48  45542  fourierdlem51  45545  fourierdlem54  45548  fourierdlem74  45568  fourierdlem77  45571  fourierdlem87  45581  fourierdlem97  45591  ioorrnopnlem  45692  ovnsubaddlem2  45959  smfinflem  46205  fsupdm  46230  finfdm  46234  eluzge0nn0  46692  fzopredsuc  46703  fzoopth  46707  imasetpreimafvbijlemfv  46742  lighneallem4  46950  oexpnegALTV  47017  oexpnegnz  47018  tgblthelfgott  47155  rmsupp0  47432  rmsuppss  47434  lincresunit3lem3  47542  lincresunit3lem2  47548  lindssnlvec  47554  fdivmptf  47614  refdivmptf  47615  elbigolo1  47630  rrx2linest  47815  itsclc0lem1  47829  itsclc0lem2  47830  itsclc0yqsollem1  47835  itsclc0b  47845