Theorem simpr3 1215

Description: Simplification of conjunction. (Contributed by Jeff Hankins, 17-Nov-2009.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)

Assertion

Ref	Expression
simpr3	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜃)

Proof of Theorem simpr3

Step	Hyp	Ref	Expression
1		simpr 490	. 2 ⊢ ((𝜑 ∧ 𝜃) → 𝜃)
2	1	3ad2antr3 1209	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simpr13  1278  simpr23  1281  simpr33  1284  simp1r3  1290  simp2r3  1296  simp3r3  1302  3anandis  1501  funopsn  7175  funopsnOLD  7176  fpr2g  7240  isopolem  7376  fr3nr  7810  sexp3  8197  suppfnss  8234  naddass  8734  dif1en  9205  elfir  9434  intrnfi  9435  fisupcl  9489  cnfcomlem  9727  ttrclss  9748  dmttrcl  9749  rnttrcl  9750  ttrclselem2  9754  ackbij1lem15  10338  pwfseqlem4a  10773  pwfseqlem4  10774  eluzuzle  13001  xlesubadd  13420  elioc2  13567  elico2  13568  elicc2  13569  fseq1p1m1  13759  ccatswrd  14846  pfxccat3a  14915  2cshw  14992  tanadd  16364  dvds2ln  16488  prmgaplem5  17262  prmgaplem8  17265  cshwsidrepsw  17300  ressress  17454  f1ovscpbl  17727  mreexexlem4d  17850  mreexexd  17851  2oppccomf  17928  fthmon  18133  fuccocl  18171  fucidcl  18172  invfuc  18181  initoeu2lem1  18218  curf2cl  18434  yonedalem4c  18480  yonedalem3  18483  pospo  18546  latjle12  18653  latjlej1  18656  latnlej2  18662  latlem12  18669  latmlem1  18672  latledi  18680  latjass  18686  latj12  18687  latj32  18688  latj13  18689  latj31  18690  latjrot  18691  latjjdi  18694  latjjdir  18695  latdisdlem  18699  prdssgrpd  18951  prdsmndd  18993  imasmnd2  18997  imasmnd  18998  frmdmnd  19084  grpsubadd  19267  grpaddsubass  19269  grpsubsub4  19272  grppnpcan2  19273  grpnpncan  19274  grpnnncan2  19276  imasgrp2  19294  imasgrp  19295  mulgnndir  19342  mulgnn0dir  19343  mulgnnass  19348  mulgnn0ass  19349  mulgass  19350  pwsmulg  19358  issubg2  19381  qusgrp  19430  kerf1ghm  19490  galcan  19548  gacan  19549  oppgmnd  19598  pmtrprfv  19697  pmtr3ncom  19719  psgnunilem3  19740  frgp0  20004  cmn32  20044  cmn12  20046  abladdsub  20056  ablsubaddsub  20058  ablsubsub23  20068  mulgdi  20070  mulgsubdi  20073  dprdss  20275  dprdf1o  20278  dprdsn  20282  dmdprdsplit  20293  pgpfac1lem5  20325  omndmul2  20377  prdsrngd  20428  imasrng  20429  srgdilem  20448  ringdilem  20506  ringrng  20544  prdsringd  20580  imasring  20590  opprrng  20605  mulgass3  20613  dvrass  20668  dvrdir  20672  subrgunit  20872  issubrg2  20874  isdomn4  20997  abvdiv  21116  lss1  21243  lsssn0  21253  islss3  21264  prdslmodd  21274  islmhm2  21343  lspsolv  21451  lbsextlem4  21469  sralmod  21492  rnglidl1  21542  prmidlc  21659  ssdifidl  21671  ipdi  21976  ipsubdir  21978  ipsubdi  21979  ipassr  21982  ipassr2  21983  isphld  21990  ocvlss  22008  sraassab  22206  psrlmod  22297  psrring  22307  psrassa  22310  mpllsslem  22337  mamudm  22740  matring  22788  matassa  22789  ofco2  22796  scmatlss  22870  ma1repveval  22916  mdetunilem1  22957  mdetunilem9  22965  monmatcollpw  23127  iinopn  23250  restopnb  23523  subbascn  23602  hausnei2  23701  nrmsep2  23704  isnrm3  23707  t1sep  23718  regsep2  23724  dnsconst  23726  dfconn2  23767  dislly  23846  tx1stc  23999  qtophmeo  24166  filss  24202  infil  24212  fsubbas  24216  filssufilg  24260  hauspwpwf1  24336  cnextcn  24416  tmdcn2  24438  psmettri  24660  isxmet2d  24676  xmettri  24700  xmetres2  24710  bldisj  24747  blss2ps  24752  blss2  24753  xmstri2  24815  mstri2  24816  xmstri  24817  mstri  24818  xmstri3  24819  mstri3  24820  msrtri  24821  comet  24862  met2ndci  24871  ngprcan  24959  ngplcan  24960  ngpsubcan  24963  nmtri2  24976  nrgdsdi  25014  nrgdsdir  25015  nlmdsdi  25030  nlmdsdir  25031  blcvx  25147  iocopnst  25291  icccvx  25301  pi1grplem  25400  pi1xfrf  25404  pi1cof  25410  clmpm1dir  25454  cmodscmulexp  25473  cvsdiv  25483  cvsdivcl  25484  cphdivcl  25533  cphsubdir  25559  cphsubdi  25560  bcthlem5  25679  rrxcph  25743  volfiniun  25898  volcn  25957  itg1val2  26035  dvconst  26267  dvlip  26343  ftc1a  26387  ulmdvlem3  26759  ang180  27172  cvxcl  27342  scvxcvx  27343  sgmmul  27558  logexprlim  27582  dchrabl  27611  nosupbnd1  28101  noinfbnd1lem5  28114  noinfbnd1  28116  sltssep  28183  addscom  28382  addbday  28434  addsdi  28571  mulsass  28582  motgrp  29036  iscgra1  29347  cgrane2  29350  cgrane4  29352  cgrahl1  29353  cgrahl2  29354  cgracgr  29355  cgratr  29360  cgrabtwn  29364  cgrahl  29365  dfcgra2  29368  sacgr  29369  angmgmaddcl  29421  f1otrge  29479  xmstrkgc  29493  colinearalglem1  29514  colinearalg  29518  axcgrtr  29523  axlowdimlem16  29565  axeuclidlem  29570  axcontlem4  29575  axcontlem7  29578  axcontlem12  29583  eengtrkg  29594  eengtrkge  29595  edglnl  29751  subgruhgredgd  29895  nbfusgrlevtxm2  29989  upgrwlkdvde  30353  crctcshwlkn0lem5  30433  crctcshwlkn0  30440  usgrwwlks2on  30577  umgrwwlks2on  30578  rusgrnumwwlks  30596  clwlkclwwlkfo  30630  3spthd  30807  frgr2wwlkeqm  30962  dlwwlknondlwlknonf1o  30996  numclwwlk5  31019  friendship  31030  grpomuldivass  31173  ablodivdiv4  31186  dipdi  31475  dipsubdi  31481  disjdsct  33367  archiabllem2c  33826  dvrcan5  33866  rloccring  33902  reofld  33974  eqgvscpbl  33981  qusvsval  33983  quslmod  33989  quslmhm  33990  ssmxidl  34069  ply1degltlss  34198  r1plmhm  34211  drgextlsp  34296  ccfldsrarelvec  34373  constrconj  34447  constrfin  34448  constrelextdg2  34449  pstmfval  34598  qqhval2lem  34683  qqhvq  34689  esumcvg  34788  sigaclcu  34819  measdivcst  34927  measdivcstALTV  34928  carsggect  35020  tgoldbachgtd  35361  bnj970  35647  bnj910  35648  erdszelem9  36131  cvmseu  36208  elmrsubrn  36452  r1peuqusdeg1  36575  cgrid2  36946  btwncomim  36956  btwnswapid  36960  trisegint  36971  cgrxfr  36998  btwnxfr  36999  brofs2  37020  brifs2  37021  endofsegid  37028  btwnconn1lem11  37040  btwnconn2  37045  segcon2  37048  seglemin  37056  segletr  37057  btwnsegle  37060  colinbtwnle  37061  broutsideof2  37065  btwnoutside  37068  broutsideof3  37069  outsideoftr  37072  outsidele  37075  ellines  37095  linethrueu  37099  nmulprop  37117  nadddi  37151  weiunpo  37431  unbdqndv2  37555  poimirlem28  38758  ftc1anc  38811  sdclem1  38869  sstotbnd2  38900  ismndo1  38999  zerdivemp1x  39073  isdrngo2  39084  iscringd  39124  lsmsat  40257  lfladdcl  40320  lflnegcl  40324  lflvscl  40326  lshpkrlem4  40362  lshpkrlem6  40364  ldualgrplem  40394  lduallmodlem  40401  latmassOLD  40478  latm12  40479  latm32  40480  latmrot  40481  latmmdiN  40483  latmmdir  40484  omlfh1N  40507  omlfh3N  40508  cvrnbtwn2  40524  cvlexchb1  40579  cvlexch3  40581  cvlexch4N  40582  cvlatexchb1  40583  cvlsupr2  40592  hlatjass  40619  hlatj12  40620  hlatj32  40621  cvrat  40671  atcvrj0  40677  cvrat2  40678  atltcvr  40684  atexchltN  40690  cvrat3  40691  cvrat4  40692  atbtwnexOLDN  40696  atbtwnex  40697  3dimlem3  40710  3dimlem3OLDN  40711  3at  40739  2atneat  40764  llncmp  40771  2at0mat0  40774  2atmat0  40775  islpln2a  40797  llncvrlpln  40807  lplncmp  40811  3atnelvolN  40835  4atlem11  40858  lplncvrlvol  40865  lvolcmp  40866  2atm2atN  41034  elpaddatriN  41052  elpadd2at2  41056  paddasslem8  41076  paddasslem17  41085  paddass  41087  padd12N  41088  paddssw1  41092  pmodlem2  41096  pmodN  41099  pmapjlln1  41104  atmod1i2  41108  pexmidlem2N  41220  pexmidlem7N  41225  pl42lem2N  41229  pl42lem3N  41230  pl42lem4N  41231  pl42N  41232  lhp2lt  41250  lhpm0atN  41278  lautlt  41340  lautcvr  41341  lautj  41342  lautm  41343  ltrneq2  41397  cdleme1b  41475  cdleme3b  41478  cdleme3c  41479  cdleme9b  41501  cdlemefs27cl  41662  cdleme42mN  41736  cdlemg4c  41861  trljco  41989  tgrpgrplem  41998  tendoplass  42032  tendodi1  42033  tendodi2  42034  erngplus2  42053  erngplus2-rN  42061  cdlemk36  42162  erngdvlem3  42239  erngdvlem3-rN  42247  dvaplusgv  42259  tendospass  42268  tendospdi1  42269  dvalveclem  42274  dialss  42295  dvhvaddass  42346  dvhopvsca  42351  dvhlveclem  42357  diblss  42419  diclss  42442  diclspsn  42443  cdlemn11pre  42459  dihmeetlem12N  42567  dihmeetlem16N  42571  dihmeetlem17N  42572  dvh4dimN  42696  lpolsatN  42737  lpolpolsatN  42738  dochpolN  42739  lclkr  42782  lclkrs  42788  lcfr  42834  lcmineqlem13  43283  aks6d1c1  43358  irrapxlem6  44027  jm2.26lem3  44201  mpaamn  44350  mendring  44382  mendlmod  44383  mendassa  44384  nnoeomeqom  44506  omabs2  44526  neicvgel1  45311  rfcnpre4  46256  fmuldfeq  46800  stoweidlem43  47258  stoweidlem52  47267  stoweidlem53  47268  stoweidlem56  47271  issmfgt  47971  issmfge  47985  tmachlem-franscan  48164  iccelpart  48720  prproropf1olem1  48790  fmtnoprmfac1  48855  fmtnoprmfac2  48857  isubgr3stgrlem2  49270  isubgr3stgrlem4  49272  grlimgrtrilem1  49304  copissgrp  49470  cznrng  49563  funcringcsetcALTV2lem9  49600  funcringcsetclem9ALTV  49623  idomcanl  49649  linccl  49731  lincsumscmcl  49750  ldepsprlem  49789  lincresunit3lem1  49796  itsclc0yqe  50078  resipos  50294  topdlat  50323  catprs  50330  endmndlem  50334  idmon  50339  idepi  50340  thincmon  50773  thincepi  50774  functhinclem1  50784  grptcmon  50936  grptcepi  50937  nellindf  51250