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  3582  2nreu  4385  f1prex  7239  weniso  7309  ofmpteq  7654  tfisi  7810  mposn  8053  fprlem1  8250  smogt  8307  smocdmdom  8308  omeulem1  8517  nnmord  8568  nnmword  8569  naddasslem1  8630  naddasslem2  8631  difsnen  8997  enfixsn  9024  mapunen  9084  ac6sfi  9194  ordiso2  9430  wemaplem2  9462  wemapso2lem  9467  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  11330  addcan2  11331  divmulass  11832  divmulasscom  11833  ltmul1a  12004  supmul1  12125  uzsupss  12890  xaddass  13201  xleadd1a  13205  xlesubadd  13215  xmulass  13239  xlemul2a  13241  xadddilem  13246  xadddi  13247  ixxdisj  13313  ixxun  13314  ixxlb  13320  icoshftf1o  13427  icodisj  13429  ioounsn  13430  lincmb01cmp  13448  iccf1o  13449  elfz1b  13547  ssfzoulel  13715  fzoopth  13717  modmuladd  13875  modaddmulmod  13900  ltexp2a  14128  leexp2  14133  ltexp2r  14135  exple1  14139  expnlbnd2  14196  mulsubdivbinom2  14224  fun2dmnop0  14466  ccatass  14551  ccatopth  14678  pfxccatin12lem2a  14689  repswpfx  14747  repswccat  14748  cshwidxmodr  14766  2cshw  14775  repsco  14802  s2f1o  14878  limsupgle  15439  limsupgre  15443  addcn2  15556  mulcn2  15558  binomrisefac  16007  dvdsval2  16224  dvdsadd2b  16275  dvdsmod  16298  oexpneg  16314  sadass  16440  gcdass  16516  rplpwr  16527  lcmass  16583  coprmdvds2  16623  rpmulgcd2  16625  rpdvds  16629  coprmprod  16630  cncongr2  16637  rpexp  16692  prmdiveq  16756  hashgcdlem  16758  odzdvds  16766  coprimeprodsq2  16780  pythagtriplem3  16789  pythagtriplem4  16790  pcdvdsb  16840  vdwnnlem1  16966  0ram  16991  ramz2  16995  ramub1lem1  16997  mremre  17566  mrieqv2d  17605  lubss  18479  lubun  18481  clatleglb  18484  clatglbss  18485  mrelatglb  18526  isnsgrp  18691  issubmnd  18729  gsumccat  18809  frmdss2  18831  submefmnd  18863  nmzsubg  19140  ghmnsgima  19215  gsmsymgreqlem1  19405  psgnunilem4  19472  odmodnn0  19515  odnncl  19520  odmod  19521  oddvds  19522  odeq  19525  odmulgid  19529  odmulgeq  19532  odbezout  19533  odf1o1  19547  odf1o2  19548  odngen  19552  gexdvdsi  19558  pgpfi1  19570  odcau  19579  subgslw  19591  fislw  19600  lsmless1x  19619  lsmless2x  19620  lsmsubm  19628  lsmmod  19650  lsmmod2  19651  efgsfo  19714  odadd1  19823  odadd2  19824  odadd  19825  lsmcomx  19831  prdscmnd  19836  gsumconst  19909  ablsimpgfindlem1  20084  srg1zr  20196  csrgbinom  20213  ring1eq0  20279  mulgass2  20290  rngisom1  20446  rhmdvdsr  20485  cntzsubrng  20544  cntzsubr  20583  isabvd  20789  rmodislmod  20925  0lmhm  21035  lmhmvsca  21040  reslmhm2b  21049  pwssplit1  21054  pwssplit2  21055  pwssplit3  21056  lbspss  21077  lspsnat  21143  lidldvgen  21332  xrsdsreclblem  21393  cssmre  21673  obs2ss  21709  uvcresum  21773  frlmsslsp  21776  frlmup4  21781  lindff1  21800  f1lindf  21802  lsslindf  21810  islindf4  21818  issubassa  21847  evlsval2  22065  coe1subfv  22231  coe1sclmul  22247  coe1sclmul2  22249  mpomatmul  22411  mamutpos  22423  scmatscmide  22472  mavmulsolcl  22516  mulmarep1gsum2  22539  mdetdiaglem  22563  mdetdiag  22564  mdetunilem1  22577  mdetunilem3  22579  mdetunilem9  22585  maducoeval2  22605  madurid  22609  slesolinvbi  22646  cramerimplem1  22648  cramerlem1  22652  cramer  22656  cpmatel2  22678  m2cpm  22706  m2pmfzmap  22712  m2cpminvid2lem  22719  m2cpminvid2  22720  decpmatmul  22737  pmatcollpw1lem2  22740  pmatcollpw1  22741  pmatcollpw2lem  22742  pmatcollpwfi  22747  pm2mpcl  22762  mply1topmatcl  22770  mp2pm2mplem2  22772  mp2pm2mplem4  22774  mp2pm2mplem5  22775  mp2pm2mp  22776  pm2mpghmlem2  22777  pm2mpghmlem1  22778  chfacfisfcpmat  22820  topssnei  23089  cnconst2  23248  cnpresti  23253  cnprest2  23255  cnpdis  23258  cnt0  23311  cnt1  23315  cnhaus  23319  sscmp  23370  hauscmp  23372  cnconn  23387  unconn  23394  finlocfin  23485  comppfsc  23497  kgen2ss  23520  ptpjopn  23577  prdstopn  23593  ptrescn  23604  qtopss  23680  kqfvima  23695  fbssint  23803  fbasrn  23849  filuni  23850  fmss  23911  rnelfm  23918  fmufil  23924  fmco  23926  flimss2  23937  flimss1  23938  flimrest  23948  cnpflf2  23965  flfcnp  23969  supnfcls  23985  fclsss1  23987  fclsss2  23988  isfcf  23999  subgntr  24072  opnsubg  24073  cldsubg  24076  ghmcnp  24080  ustuqtop1  24206  bldisj  24363  blgt0  24364  bl2in  24365  blss2ps  24368  blss2  24369  blssps  24389  blss  24390  xmetresbl  24402  lpbl  24468  blcld  24470  stdbdmopn  24483  metcnp3  24505  metcnp  24506  metcnp2  24507  txmetcnp  24512  blval2  24527  nmoix  24694  nmoi2  24695  nmotri  24704  metdsge  24815  metdseq0  24820  iocopnst  24907  xrhmeo  24913  nmhmcn  25087  cphsqrtcl2  25153  cphsqrtcl3  25154  cssbn  25342  pjth  25406  ovoliunlem2  25470  volun  25512  mbfimaopn2  25624  iblconst  25785  limcvallem  25838  dvfval  25864  dvcnp2  25887  dvcn  25888  deg1mul3le  26082  deg1tmle  26083  dvdsq1p  26128  idomrootle  26138  ig1peu  26140  ig1pdvds  26145  ply1term  26169  coeid3  26205  dgrmulc  26236  dvply1  26250  aaliou2  26306  efcvx  26414  tanord  26502  eflogeq  26566  logdivlti  26584  logccv  26627  recxpcl  26639  cxplea  26660  cxpeq  26721  ang180  26778  isosctrlem2  26783  cxp2lim  26940  amgm  26954  muval1  27096  dvdssqf  27101  mumullem2  27143  mumul  27144  bcmono  27240  lgsneg  27284  lgsdilem  27287  lgsdirprm  27294  lgsdir  27295  lgsdi  27297  lgsne0  27298  nolesgn2o  27635  nogesgn1o  27637  nosep1o  27645  nosep2o  27646  nosepssdm  27650  nosupres  27671  nosupbnd1lem1  27672  nosupbnd1lem4  27675  nosupbnd1lem5  27676  nosupbnd1lem6  27677  noinfres  27686  noinfbnd1lem1  27687  noinfbnd1lem4  27690  noinfbnd1lem6  27692  noinfbnd2  27695  noetasuplem3  27699  noetainflem3  27703  leslss  27901  cofslts  27910  coinitslts  27911  cofcutrtime  27919  addsass  27997  addsdi  28147  mulsass  28158  ltmuls2  28163  divmulsw  28185  bdayfinbndlem1  28459  z12bdaylem  28476  brbtwn2  28974  colinearalglem1  28975  colinearalg  28979  axcgrtr  28984  axsegconlem8  28993  axsegconlem9  28994  axsegconlem10  28995  axcontlem2  29034  axcontlem10  29042  elntg2  29054  ewlkle  29674  crctcshwlkn0lem5  29882  wwlknp  29911  wwlksnext  29961  wwlksnextproplem1  29977  wspthsnwspthsnon  29984  clwlkclwwlklem3  30071  erclwwlksym  30091  erclwwlknsym  30140  upgriseupth  30277  eucrct2eupth  30315  3cyclfrgrrn  30356  numclwwlk2lem1lem  30412  numclwwlk1lem2foa  30424  frgrregord13  30466  nvmul0or  30721  ipval2lem2  30775  lnoadd  30829  lnosub  30830  lnomul  30831  shless  31430  shlej1  31431  kbmul  32026  homco2  32048  kbass2  32188  eliccelico  32850  elicoelioo  32851  iocinioc2  32852  iocinif  32854  difioo  32855  nexple  32917  swrdrn2  33014  swrdrn3  33015  xrge0adddir  33078  xrge0npcan  33080  isarchi2  33246  archiabl  33259  pidlnz  33436  lindssn  33438  ssmxidl  33534  pstmfval  34040  fmcncfil  34075  zrhnm  34111  qqhnm  34134  volfiniune  34374  dya2iocnrect  34425  probinc  34565  cndprob01  34579  signswmnd  34701  bnj517  35027  cvmsss2  35456  cvmlift2lem10  35494  br6  35939  funsseq  35950  cgrtriv  36184  5segofs  36188  btwnouttr2  36204  btwnxfr  36238  lineext  36258  btwnconn1lem13  36281  brsegle2  36291  nn0prpwlem  36504  weiunpo  36647  weiunso  36648  weiunfr  36649  weiunse  36650  axtcond  36660  lindsenlbs  37936  blbnd  38108  ismtyima  38124  rrndstprj2  38152  ghomdiv  38213  grpokerinj  38214  lsatfixedN  39455  lssat  39462  lshpkrlem4  39559  cvrcon3b  39723  atlen0  39756  atcvreq0  39760  atnle  39763  atlatmstc  39765  atlatle  39766  cvlcvr1  39785  hlsupr2  39833  hlrelat2  39849  cvrexchlem  39865  lnnat  39873  atcvrj2b  39878  3dimlem3  39907  3dim1  39913  1cvrjat  39921  llni  39954  llni2  39958  llnexatN  39967  2llnmat  39970  lplni  39978  2atnelpln  39990  llncvrlpln2  40003  2llnmj  40006  lplnexatN  40009  lplnexllnN  40010  2llnm3N  40015  lvoli  40021  lvoli3  40023  lvolnle3at  40028  islvol2aN  40038  4atlem4a  40045  4atlem4b  40046  4atlem11  40055  lplncvrlvol2  40061  2lplnmj  40068  islinei  40186  linepmap  40221  lnjatN  40226  lncvrat  40228  lncmp  40229  elpaddn0  40246  elpaddatriN  40249  elpaddat  40250  paddcom  40259  paddss2  40264  paddss12  40265  paddasslem4  40269  paddasslem9  40274  paddasslem10  40275  pmodl42N  40297  pmapjoin  40298  llnmod1i2  40306  polcon2bN  40366  pclfinclN  40396  poml4N  40399  poml6N  40401  osumcllem1N  40402  osumcllem2N  40403  osumcllem11N  40412  osumclN  40413  pmapojoinN  40414  pexmidlem2N  40417  pexmidlem3N  40418  pexmidlem4N  40419  pexmidlem6N  40421  pexmidlem7N  40422  pl42lem2N  40426  pl42lem3N  40427  pl42lem4N  40428  pl42N  40429  lhprelat3N  40486  4atex  40522  lauteq  40541  lautco  40543  ltrncoidN  40574  ltrneq2  40594  ltrnideq  40621  trlnle  40632  trlval3  40633  cdlemc  40643  cdlemd9  40652  cdlemd  40653  cdleme21j  40782  cdleme21  40783  cdleme29ex  40820  cdlemefr27cl  40849  cdlemefs27cl  40859  cdleme32d  40890  cdleme32f  40892  cdleme35h2  40903  cdleme40m  40913  cdleme17d3  40942  cdleme48fvg  40946  cdlemeg46fvcl  40952  cdlemeg46fgN  40980  cdleme48fgv  40984  cdleme50trn3  40999  cdlemb3  41052  cdlemg8  41077  cdlemg11a  41083  cdlemg15a  41101  cdlemg15  41102  cdlemg16  41103  cdlemg16z  41105  cdlemg17dN  41109  cdlemg24  41134  cdlemg37  41135  cdlemg29  41151  cdlemg33b  41153  cdlemg38  41161  cdlemg40  41163  trlco  41173  cdlemg44b  41178  ltrncom  41184  trljco  41186  tendococl  41218  tendoplcl  41227  tendoplcom  41228  cdlemj2  41268  tendoid0  41271  tendo1ne0  41274  cdlemk25-3  41350  cdlemk36  41359  cdlemkid4  41380  cdlemk19x  41389  cdlemk53  41403  cdlemk56  41417  cdleml5N  41426  tendospcanN  41469  cdlemm10N  41564  dihord6apre  41702  dihord  41710  dihmeetlem1N  41736  dihglblem2N  41740  dihmeetlem2N  41745  dihmeetbN  41749  dihmeetlem5  41754  dihmeetlem6  41755  dihmeetlem7N  41756  dihmeetlem10N  41762  dihmeetlem12N  41764  dihmeetlem16N  41768  dihmeetlem17N  41769  dihmeetlem18N  41770  dihmeetALTN  41773  dihlspsnssN  41778  dvh3dim2  41894  dvh3dim3N  41895  lcfrlem16  42004  mapdrvallem2  42091  mapdh8ad  42225  hgmapvvlem3  42371  sticksstones1  42585  sticksstones2  42586  aks6d1c6isolem1  42613  resubcan2  42820  diophrw  43191  eldioph2lem1  43192  diophrex  43207  rencldnfi  43249  pellexlem2  43258  pellqrexplicit  43305  infmrgelbi  43306  pellfundglb  43313  pellfund14gap  43315  rmxycomplete  43345  congadd  43394  acongeq  43411  jm2.19  43421  jm2.23  43424  jm2.20nn  43425  jm2.27  43436  jm3.1  43448  lnmepi  43513  lmhmlnmsplit  43515  hbtlem2  43552  dgraa0p  43577  proot1hash  43623  iocunico  43639  iocinico  43640  oasubex  43714  cantnf2  43753  onmcl  43759  omcl2  43761  nadd2rabex  43814  nadd1rabtr  43816  nadd1rabex  43818  fzunt  43882  relexpxpmin  44144  ntrclsk3  44497  grur1cld  44659  ismnu  44688  grumnudlem  44712  ismnushort  44728  rfcnnnub  45467  uzwo4  45484  wessf1ornlem  45615  supxrge  45768  infleinflem2  45800  iccintsng  45953  climsuse  46038  lptre2pt  46068  limcleqr  46072  0ellimcdiv  46077  fnlimfvre  46102  dvnprodlem1  46374  volioc  46400  stoweidlem17  46445  stoweidlem19  46447  stoweidlem20  46448  stoweidlem22  46450  stoweidlem28  46456  stoweidlem34  46462  stoweidlem44  46472  stoweidlem60  46488  wallispilem3  46495  fourierdlem42  46577  fourierdlem48  46582  fourierdlem51  46585  fourierdlem54  46588  fourierdlem74  46608  fourierdlem77  46611  fourierdlem87  46621  fourierdlem97  46631  ioorrnopnlem  46732  ovnsubaddlem2  46999  smfinflem  47245  fsupdm  47270  finfdm  47274  eluzge0nn0  47754  fzopredsuc  47766  imasetpreimafvbijlemfv  47856  lighneallem4  48067  oexpnegALTV  48147  oexpnegnz  48148  tgblthelfgott  48285  clnbgrgrim  48404  isubgr3stgrlem3  48438  rmsupp0  48838  rmsuppss  48840  lincresunit3lem3  48944  lincresunit3lem2  48950  lindssnlvec  48956  fdivmptf  49011  refdivmptf  49012  elbigolo1  49027  rrx2linest  49212  itsclc0lem1  49226  itsclc0lem2  49227  itsclc0yqsollem1  49232  itsclc0b  49242  setc1onsubc  50071