Theorem simpl2 1189

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

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

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 1086

This theorem is referenced by:  simpl12  1246  simpl22  1249  simpl32  1252  simp1l2  1264  simp2l2  1270  simp3l2  1276  3anandirs  1468  rspc3ev  3621  2nreu  4434  f1prex  7275  weniso  7344  ofmpteq  7686  tfisi  7842  mposn  8084  fprlem1  8281  smogt  8363  smocdmdom  8364  omeulem1  8578  nnmord  8628  nnmword  8629  naddasslem1  8690  naddasslem2  8691  difsnen  9050  enfixsn  9078  mapunen  9143  ac6sfi  9284  ordiso2  9507  wemaplem2  9539  wemapso2lem  9544  en2eqpr  9999  acndom  10043  infmap2  10210  cflim2  10255  cfsmolem  10262  coftr  10265  fin23lem26  10317  isf32lem9  10353  fin1a2lem9  10400  fin1a2lem10  10401  gchdomtri  10621  canth4  10639  gchpwdom  10662  gruima  10794  grudomon  10809  prn0  10981  distrlem4pr  11018  prlem934  11025  addcan  11397  addcan2  11398  divmulass  11894  divmulasscom  11895  ltmul1a  12062  supmul1  12182  uzsupss  12923  xaddass  13229  xleadd1a  13233  xlesubadd  13243  xmulass  13267  xlemul2a  13269  xadddilem  13274  xadddi  13275  ixxdisj  13340  ixxun  13341  ixxlb  13347  icoshftf1o  13452  icodisj  13454  ioounsn  13455  lincmb01cmp  13473  iccf1o  13474  elfz1b  13571  ssfzoulel  13727  modmuladd  13879  modaddmulmod  13904  ltexp2a  14132  leexp2  14137  ltexp2r  14139  exple1  14142  expnlbnd2  14198  mulsubdivbinom2  14223  fun2dmnop0  14457  ccatass  14540  ccatopth  14668  pfxccatin12lem2a  14679  repswpfx  14737  repswccat  14738  cshwidxmodr  14756  2cshw  14765  repsco  14793  s2f1o  14869  limsupgle  15423  limsupgre  15427  addcn2  15540  mulcn2  15542  binomrisefac  15988  dvdsval2  16203  dvdsadd2b  16252  dvdsmod  16275  oexpneg  16291  sadass  16415  gcdass  16492  rplpwr  16502  lcmass  16554  coprmdvds2  16594  rpmulgcd2  16596  rpdvds  16600  coprmprod  16601  cncongr2  16608  rpexp  16663  prmdiveq  16724  hashgcdlem  16726  odzdvds  16733  coprimeprodsq2  16747  pythagtriplem3  16756  pythagtriplem4  16757  pcdvdsb  16807  vdwnnlem1  16933  0ram  16958  ramz2  16962  ramub1lem1  16964  mremre  17553  mrieqv2d  17588  lubss  18474  lubun  18476  clatleglb  18479  clatglbss  18480  mrelatglb  18521  isnsgrp  18652  issubmnd  18690  gsumccat  18762  frmdss2  18784  submefmnd  18816  nmzsubg  19088  ghmnsgima  19161  gsmsymgreqlem1  19346  psgnunilem4  19413  odmodnn0  19456  odnncl  19461  odmod  19462  oddvds  19463  odeq  19466  odmulgid  19470  odmulgeq  19473  odbezout  19474  odf1o1  19488  odf1o2  19489  odngen  19493  gexdvdsi  19499  pgpfi1  19511  odcau  19520  subgslw  19532  fislw  19541  lsmless1x  19560  lsmless2x  19561  lsmsubm  19569  lsmmod  19591  lsmmod2  19592  efgsfo  19655  odadd1  19764  odadd2  19765  odadd  19766  lsmcomx  19772  prdscmnd  19777  gsumconst  19850  ablsimpgfindlem1  20025  srg1zr  20116  csrgbinom  20133  ring1eq0  20193  mulgass2  20204  rngisom1  20364  rhmdvdsr  20406  cntzsubrng  20463  cntzsubr  20504  isabvd  20659  rmodislmod  20772  rmodislmodOLD  20773  0lmhm  20884  lmhmvsca  20889  reslmhm2b  20898  pwssplit1  20903  pwssplit2  20904  pwssplit3  20905  lbspss  20926  lspsnat  20992  lidldvgen  21183  xrsdsreclblem  21296  cssmre  21575  obs2ss  21613  uvcresum  21677  frlmsslsp  21680  frlmup4  21685  lindff1  21704  f1lindf  21706  lsslindf  21714  islindf4  21722  issubassa  21750  evlsval2  21981  coe1subfv  22129  coe1sclmul  22145  coe1sclmul2  22147  mpomatmul  22292  mamutpos  22304  scmatscmide  22353  mavmulsolcl  22397  mulmarep1gsum2  22420  mdetdiaglem  22444  mdetdiag  22445  mdetunilem1  22458  mdetunilem3  22460  mdetunilem9  22466  maducoeval2  22486  madurid  22490  slesolinvbi  22527  cramerimplem1  22529  cramerlem1  22533  cramer  22537  cpmatel2  22559  m2cpm  22587  m2pmfzmap  22593  m2cpminvid2lem  22600  m2cpminvid2  22601  decpmatmul  22618  pmatcollpw1lem2  22621  pmatcollpw1  22622  pmatcollpw2lem  22623  pmatcollpwfi  22628  pm2mpcl  22643  mply1topmatcl  22651  mp2pm2mplem2  22653  mp2pm2mplem4  22655  mp2pm2mplem5  22656  mp2pm2mp  22657  pm2mpghmlem2  22658  pm2mpghmlem1  22659  chfacfisfcpmat  22701  topssnei  22972  cnconst2  23131  cnpresti  23136  cnprest2  23138  cnpdis  23141  cnt0  23194  cnt1  23198  cnhaus  23202  sscmp  23253  hauscmp  23255  cnconn  23270  unconn  23277  finlocfin  23368  comppfsc  23380  kgen2ss  23403  ptpjopn  23460  prdstopn  23476  ptrescn  23487  qtopss  23563  kqfvima  23578  fbssint  23686  fbasrn  23732  filuni  23733  fmss  23794  rnelfm  23801  fmufil  23807  fmco  23809  flimss2  23820  flimss1  23821  flimrest  23831  cnpflf2  23848  flfcnp  23852  supnfcls  23868  fclsss1  23870  fclsss2  23871  isfcf  23882  subgntr  23955  opnsubg  23956  cldsubg  23959  ghmcnp  23963  ustuqtop1  24090  bldisj  24248  blgt0  24249  bl2in  24250  blss2ps  24253  blss2  24254  blssps  24274  blss  24275  xmetresbl  24287  lpbl  24356  blcld  24358  stdbdmopn  24371  metcnp3  24393  metcnp  24394  metcnp2  24395  txmetcnp  24400  blval2  24415  nmoix  24590  nmoi2  24591  nmotri  24600  metdsge  24709  metdseq0  24714  iocopnst  24808  xrhmeo  24815  nmhmcn  24991  cphsqrtcl2  25058  cphsqrtcl3  25059  cssbn  25247  pjth  25311  ovoliunlem2  25376  volun  25418  mbfimaopn2  25530  iblconst  25691  limcvallem  25744  dvfval  25770  dvcnp2  25793  dvcnp2OLD  25794  dvcn  25795  deg1mul3le  25996  deg1tmle  25997  dvdsq1p  26041  idomrootle  26051  ig1peu  26053  ig1pdvds  26058  ply1term  26082  coeid3  26118  dgrmulc  26150  dvply1  26162  aaliou2  26218  efcvx  26327  tanord  26413  eflogeq  26477  logdivlti  26495  logccv  26538  recxpcl  26550  cxplea  26571  cxpeq  26633  ang180  26687  isosctrlem2  26692  cxp2lim  26850  amgm  26864  muval1  27006  dvdssqf  27011  mumullem2  27053  mumul  27054  bcmono  27151  lgsneg  27195  lgsdilem  27198  lgsdirprm  27205  lgsdir  27206  lgsdi  27208  lgsne0  27209  nolesgn2o  27545  nogesgn1o  27547  nosep1o  27555  nosep2o  27556  nosepssdm  27560  nosupres  27581  nosupbnd1lem1  27582  nosupbnd1lem4  27585  nosupbnd1lem5  27586  nosupbnd1lem6  27587  noinfres  27596  noinfbnd1lem1  27597  noinfbnd1lem4  27600  noinfbnd1lem6  27602  noinfbnd2  27605  noetasuplem3  27609  noetainflem3  27613  slelss  27775  cofsslt  27779  coinitsslt  27780  cofcutrtime  27788  addsass  27863  addsdi  27996  mulsass  28007  sltmul2  28012  divsmulw  28033  brbtwn2  28657  colinearalglem1  28658  colinearalg  28662  axcgrtr  28667  axsegconlem8  28676  axsegconlem9  28677  axsegconlem10  28678  axcontlem2  28717  axcontlem10  28725  elntg2  28737  ewlkle  29357  crctcshwlkn0lem5  29563  wwlknp  29592  wwlksnext  29642  wwlksnextproplem1  29658  wspthsnwspthsnon  29665  clwlkclwwlklem3  29749  erclwwlksym  29769  erclwwlknsym  29818  upgriseupth  29955  eucrct2eupth  29993  3cyclfrgrrn  30034  numclwwlk2lem1lem  30090  numclwwlk1lem2foa  30102  frgrregord13  30144  nvmul0or  30398  ipval2lem2  30452  lnoadd  30506  lnosub  30507  lnomul  30508  shless  31107  shlej1  31108  kbmul  31703  homco2  31725  kbass2  31865  eliccelico  32483  elicoelioo  32484  iocinioc2  32485  iocinif  32487  difioo  32488  swrdrn2  32611  swrdrn3  32612  xrge0adddir  32684  xrge0npcan  32686  isarchi2  32825  archiabl  32838  pidlnz  32984  lindssn  32990  ssmxidl  33086  pstmfval  33396  fmcncfil  33431  zrhnm  33469  qqhnm  33490  nexple  33527  volfiniune  33748  dya2iocnrect  33800  probinc  33940  cndprob01  33954  signswmnd  34088  bnj517  34415  cvmsss2  34783  cvmlift2lem10  34821  br6  35250  funsseq  35262  cgrtriv  35497  5segofs  35501  btwnouttr2  35517  btwnxfr  35551  lineext  35571  btwnconn1lem13  35594  brsegle2  35604  nn0prpwlem  35708  lindsenlbs  36987  blbnd  37159  ismtyima  37175  rrndstprj2  37203  ghomdiv  37264  grpokerinj  37265  lsatfixedN  38383  lssat  38390  lshpkrlem4  38487  cvrcon3b  38651  atlen0  38684  atcvreq0  38688  atnle  38691  atlatmstc  38693  atlatle  38694  cvlcvr1  38713  hlsupr2  38762  hlrelat2  38778  cvrexchlem  38794  lnnat  38802  atcvrj2b  38807  3dimlem3  38836  3dim1  38842  1cvrjat  38850  llni  38883  llni2  38887  llnexatN  38896  2llnmat  38899  lplni  38907  2atnelpln  38919  llncvrlpln2  38932  2llnmj  38935  lplnexatN  38938  lplnexllnN  38939  2llnm3N  38944  lvoli  38950  lvoli3  38952  lvolnle3at  38957  islvol2aN  38967  4atlem4a  38974  4atlem4b  38975  4atlem11  38984  lplncvrlvol2  38990  2lplnmj  38997  islinei  39115  linepmap  39150  lnjatN  39155  lncvrat  39157  lncmp  39158  elpaddn0  39175  elpaddatriN  39178  elpaddat  39179  paddcom  39188  paddss2  39193  paddss12  39194  paddasslem4  39198  paddasslem9  39203  paddasslem10  39204  pmodl42N  39226  pmapjoin  39227  llnmod1i2  39235  polcon2bN  39295  pclfinclN  39325  poml4N  39328  poml6N  39330  osumcllem1N  39331  osumcllem2N  39332  osumcllem11N  39341  osumclN  39342  pmapojoinN  39343  pexmidlem2N  39346  pexmidlem3N  39347  pexmidlem4N  39348  pexmidlem6N  39350  pexmidlem7N  39351  pl42lem2N  39355  pl42lem3N  39356  pl42lem4N  39357  pl42N  39358  lhprelat3N  39415  4atex  39451  lauteq  39470  lautco  39472  ltrncoidN  39503  ltrneq2  39523  ltrnideq  39550  trlnle  39561  trlval3  39562  cdlemc  39572  cdlemd9  39581  cdlemd  39582  cdleme21j  39711  cdleme21  39712  cdleme29ex  39749  cdlemefr27cl  39778  cdlemefs27cl  39788  cdleme32d  39819  cdleme32f  39821  cdleme35h2  39832  cdleme40m  39842  cdleme17d3  39871  cdleme48fvg  39875  cdlemeg46fvcl  39881  cdlemeg46fgN  39909  cdleme48fgv  39913  cdleme50trn3  39928  cdlemb3  39981  cdlemg8  40006  cdlemg11a  40012  cdlemg15a  40030  cdlemg15  40031  cdlemg16  40032  cdlemg16z  40034  cdlemg17dN  40038  cdlemg24  40063  cdlemg37  40064  cdlemg29  40080  cdlemg33b  40082  cdlemg38  40090  cdlemg40  40092  trlco  40102  cdlemg44b  40107  ltrncom  40113  trljco  40115  tendococl  40147  tendoplcl  40156  tendoplcom  40157  cdlemj2  40197  tendoid0  40200  tendo1ne0  40203  cdlemk25-3  40279  cdlemk36  40288  cdlemkid4  40309  cdlemk19x  40318  cdlemk53  40332  cdlemk56  40346  cdleml5N  40355  tendospcanN  40398  cdlemm10N  40493  dihord6apre  40631  dihord  40639  dihmeetlem1N  40665  dihglblem2N  40669  dihmeetlem2N  40674  dihmeetbN  40678  dihmeetlem5  40683  dihmeetlem6  40684  dihmeetlem7N  40685  dihmeetlem10N  40691  dihmeetlem12N  40693  dihmeetlem16N  40697  dihmeetlem17N  40698  dihmeetlem18N  40699  dihmeetALTN  40702  dihlspsnssN  40707  dvh3dim2  40823  dvh3dim3N  40824  lcfrlem16  40933  mapdrvallem2  41020  mapdh8ad  41154  hgmapvvlem3  41300  sticksstones1  41497  sticksstones2  41498  resubcan2  41813  diophrw  42049  eldioph2lem1  42050  diophrex  42065  rencldnfi  42111  pellexlem2  42120  pellqrexplicit  42167  infmrgelbi  42168  pellfundglb  42175  pellfund14gap  42177  rmxycomplete  42208  congadd  42257  acongeq  42274  jm2.19  42284  jm2.23  42287  jm2.20nn  42288  jm2.27  42299  jm3.1  42311  lnmepi  42379  lmhmlnmsplit  42381  hbtlem2  42418  dgraa0p  42443  proot1hash  42493  iocunico  42510  iocinico  42511  oasubex  42586  cantnf2  42625  onmcl  42631  omcl2  42633  nadd2rabex  42686  nadd1rabtr  42688  nadd1rabex  42690  fzunt  42756  relexpxpmin  43018  ntrclsk3  43371  grur1cld  43541  ismnu  43570  grumnudlem  43594  ismnushort  43610  rfcnnnub  44270  uzwo4  44289  wessf1ornlem  44430  supxrge  44594  infleinflem2  44627  iccintsng  44782  climsuse  44870  lptre2pt  44902  limcleqr  44906  0ellimcdiv  44911  fnlimfvre  44936  dvnprodlem1  45208  volioc  45234  stoweidlem17  45279  stoweidlem19  45281  stoweidlem20  45282  stoweidlem22  45284  stoweidlem28  45290  stoweidlem34  45296  stoweidlem44  45306  stoweidlem60  45322  wallispilem3  45329  fourierdlem42  45411  fourierdlem48  45416  fourierdlem51  45419  fourierdlem54  45422  fourierdlem74  45442  fourierdlem77  45445  fourierdlem87  45455  fourierdlem97  45465  ioorrnopnlem  45566  ovnsubaddlem2  45833  smfinflem  46079  fsupdm  46104  finfdm  46108  eluzge0nn0  46566  fzopredsuc  46577  fzoopth  46581  imasetpreimafvbijlemfv  46616  lighneallem4  46824  oexpnegALTV  46891  oexpnegnz  46892  tgblthelfgott  47029  rmsupp0  47294  rmsuppss  47296  lincresunit3lem3  47404  lincresunit3lem2  47410  lindssnlvec  47416  fdivmptf  47476  refdivmptf  47477  elbigolo1  47492  rrx2linest  47677  itsclc0lem1  47691  itsclc0lem2  47692  itsclc0yqsollem1  47697  itsclc0b  47707