Theorem simpr3 1062

Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)

Assertion

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

Proof of Theorem simpr3

Step	Hyp	Ref	Expression
1		simp3 1056	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜃)
2	1	adantl 481	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  simplr3  1098  simprr3  1104  simp1r3  1152  simp2r3  1158  simp3r3  1164  3anandis  1426  funopsn  6319  fpr2g  6380  isopolem  6495  fr3nr  6871  suppfnss  7207  elfir  8204  intrnfi  8205  fisupcl  8258  cnfcomlem  8479  ackbij1lem15  8939  pwfseqlem4a  9362  pwfseqlem4  9363  eluzuzle  11572  xlesubadd  11965  elioc2  12107  elico2  12108  elicc2  12109  fseq1p1m1  12283  ccatswrd  13308  modfsummods  14366  tanadd  14736  dvds2ln  14852  prmgaplem5  15597  prmgaplem8  15600  cshwsidrepsw  15638  ressress  15765  f1ovscpbl  16009  mreexexlem4d  16130  mreexexd  16131  mreexexdOLD  16132  2oppccomf  16208  fthmon  16410  fuccocl  16447  fucidcl  16448  invfuc  16457  initoeu2lem1  16487  curf2cl  16694  yonedalem4c  16740  yonedalem3  16743  pospo  16796  latjle12  16885  latjlej1  16888  latnlej2  16894  latlem12  16901  latmlem1  16904  latledi  16912  latjass  16918  latj12  16919  latj32  16920  latj13  16921  latj31  16922  latjrot  16923  latjjdi  16926  latjjdir  16927  latdisdlem  17012  prdsmndd  17146  imasmnd2  17150  imasmnd  17151  frmdmnd  17219  grpsubadd  17326  grpaddsubass  17328  grpsubsub4  17331  grppnpcan2  17332  grpnpncan  17333  grpnnncan2  17335  imasgrp2  17353  imasgrp  17354  mulgnndir  17392  mulgnndirOLD  17393  mulgnn0dir  17394  mulgnnass  17399  mulgnnassOLD  17400  mulgnn0ass  17401  mulgass  17402  pwsmulg  17410  issubg2  17432  qusgrp  17472  galcan  17560  gacan  17561  oppgmnd  17607  symggrp  17643  pmtrprfv  17696  pmtr3ncom  17718  psgnunilem3  17739  frgp0  17996  cmn32  18034  cmn12  18036  abladdsub  18043  ablsubsub23  18053  mulgdi  18055  mulgsubdi  18058  dprdss  18251  dprdf1o  18254  dprdsn  18258  dmdprdsplit  18269  pgpfac1lem5  18301  srgi  18334  ringi  18383  prdsringd  18435  imasring  18442  opprring  18454  mulgass3  18460  dvrass  18513  kerf1hrm  18566  subrgunit  18621  issubrg2  18623  abvdiv  18660  lss1  18760  lsssn0  18769  islss3  18780  prdslmodd  18790  islmhm2  18859  lspsolv  18964  lbsextlem4  18982  sralmod  19008  issubassa  19145  sraassa  19146  psrbaglesupp  19189  psrbagcon  19192  psrgrp  19219  psrlmod  19222  psrring  19232  psrassa  19235  mpllsslem  19256  ipdi  19804  ipsubdir  19806  ipsubdi  19807  ipassr  19810  ipassr2  19811  isphld  19818  ocvlss  19835  mamudm  20013  matring  20068  matassa  20069  ofco2  20076  scmatlss  20150  ma1repveval  20196  mdetunilem1  20237  mdetunilem9  20245  monmatcollpw  20403  iinopn  20532  restopnb  20789  subbascn  20868  nrmsep2  20970  isnrm3  20973  t1sep  20984  regsep2  20990  dnsconst  20992  dfcon2  21032  dislly  21110  tx1stc  21263  qtophmeo  21430  filss  21467  infil  21477  fsubbas  21481  filssufilg  21525  hauspwpwf1  21601  cnextcn  21681  tmdcn2  21703  psmettri  21926  isxmet2d  21942  xmettri  21966  xmetres2  21976  bldisj  22013  blss2ps  22018  blss2  22019  xmstri2  22081  mstri2  22082  xmstri  22083  mstri  22084  xmstri3  22085  mstri3  22086  msrtri  22087  comet  22128  met2ndci  22137  ngprcan  22224  ngplcan  22225  ngpsubcan  22228  nmtri2  22241  nrgdsdi  22279  nrgdsdir  22280  nlmdsdi  22295  nlmdsdir  22296  blcvx  22409  iocopnst  22547  icccvx  22557  pi1grplem  22657  pi1xfrf  22661  pi1cof  22667  clmpm1dir  22711  cmodscmulexp  22730  cvsdiv  22740  cvsdivcl  22741  cphdivcl  22790  cphsubdir  22816  cphsubdi  22817  bcthlem5  22933  rrxcph  22988  volfiniun  23122  volcn  23180  itg1val2  23257  dvconst  23486  dvlip  23560  ftc1a  23604  ulmdvlem3  23960  ang180  24344  cvxcl  24511  scvxcvx  24512  sgmmul  24726  logexprlim  24750  dchrabl  24779  motgrp  25238  iscgra1  25502  cgrane2  25505  cgrane4  25507  cgrahl1  25508  cgrahl2  25509  cgracgr  25510  cgratr  25515  cgrabtwn  25517  cgrahl  25518  dfcgra2  25521  sacgr  25522  f1otrge  25552  xmstrkgc  25566  colinearalglem1  25586  colinearalg  25590  axcgrtr  25595  axlowdimlem16  25637  axeuclidlem  25642  axcontlem4  25647  axcontlem7  25650  axcontlem12  25655  eengtrkg  25665  eengtrkge  25666  structiedg0val  25699  isspthonpth  26114  wlkdvspth  26138  usg2wotspth  26411  2pthwlkonot  26412  rusgranumwwlkg  26486  numclwwlk5  26639  friendship  26649  grpomuldivass  26779  ablodivdiv4  26792  ablonnncan  26794  dipdi  27082  dipsubdi  27088  disjdsct  28863  omndmul2  29043  archiabllem2c  29080  dvrdir  29121  dvrcan5  29124  reofld  29171  pstmfval  29267  qqhval2lem  29353  qqhvq  29359  esumcvg  29475  sigaclcu  29507  measdivcstOLD  29614  measdivcst  29615  carsggect  29707  bnj970  30271  bnj910  30272  erdszelem9  30435  cvmseu  30512  elmrsubrn  30671  cgrid2  31280  btwncomim  31290  btwnswapid  31294  trisegint  31305  cgrxfr  31332  btwnxfr  31333  brofs2  31354  brifs2  31355  endofsegid  31362  btwnconn1lem11  31374  btwnconn2  31379  segcon2  31382  seglemin  31390  segletr  31391  btwnsegle  31394  colinbtwnle  31395  broutsideof2  31399  btwnoutside  31402  broutsideof3  31403  outsideoftr  31406  outsidele  31409  ellines  31429  linethrueu  31433  unbdqndv2  31672  poimirlem28  32607  ftc1anc  32663  sdclem1  32709  sstotbnd2  32743  ismndo1  32842  zerdivemp1x  32916  isdrngo2  32927  iscringd  32967  lsmsat  33313  lfladdcl  33376  lflnegcl  33380  lflvscl  33382  lshpkrlem4  33418  lshpkrlem6  33420  ldualgrplem  33450  lduallmodlem  33457  latmassOLD  33534  latm12  33535  latm32  33536  latmrot  33537  latmmdiN  33539  latmmdir  33540  omlfh1N  33563  omlfh3N  33564  cvrnbtwn2  33580  cvlexchb1  33635  cvlexch3  33637  cvlexch4N  33638  cvlatexchb1  33639  cvlsupr2  33648  hlatjass  33674  hlatj12  33675  hlatj32  33676  cvrat  33726  atcvrj0  33732  cvrat2  33733  atltcvr  33739  atexchltN  33745  cvrat3  33746  cvrat4  33747  atbtwnexOLDN  33751  atbtwnex  33752  3dimlem3  33765  3dimlem3OLDN  33766  3at  33794  2atneat  33819  llncmp  33826  2at0mat0  33829  2atmat0  33830  islpln2a  33852  llncvrlpln  33862  lplncmp  33866  3atnelvolN  33890  4atlem11  33913  lplncvrlvol  33920  lvolcmp  33921  2atm2atN  34089  elpaddatriN  34107  elpadd2at2  34111  paddasslem8  34131  paddasslem17  34140  paddass  34142  padd12N  34143  paddssw1  34147  pmodlem2  34151  pmodN  34154  pmapjlln1  34159  atmod1i2  34163  pexmidlem2N  34275  pexmidlem7N  34280  pl42lem2N  34284  pl42lem3N  34285  pl42lem4N  34286  pl42N  34287  lhp2lt  34305  lhpm0atN  34333  lautlt  34395  lautcvr  34396  lautj  34397  lautm  34398  ltrneq2  34452  cdleme1b  34531  cdleme3b  34534  cdleme3c  34535  cdleme9b  34557  cdlemefs27cl  34719  cdleme42mN  34793  cdlemg4c  34918  trljco  35046  tgrpgrplem  35055  tendoplass  35089  tendodi1  35090  tendodi2  35091  erngplus2  35110  erngplus2-rN  35118  cdlemk36  35219  erngdvlem3  35296  erngdvlem3-rN  35304  dvaplusgv  35316  tendospass  35326  tendospdi1  35327  dvalveclem  35332  dialss  35353  dvhvaddass  35404  dvhopvsca  35409  dvhlveclem  35415  diblss  35477  diclss  35500  diclspsn  35501  cdlemn11pre  35517  dihmeetlem12N  35625  dihmeetlem16N  35629  dihmeetlem17N  35630  dvh4dimN  35754  lpolsatN  35795  lpolpolsatN  35796  dochpolN  35797  lclkr  35840  lclkrs  35846  lcfr  35892  irrapxlem6  36409  jm2.26lem3  36586  mpaamn  36745  mendring  36781  mendlmod  36782  mendassa  36783  neicvgel1  37437  rfcnpre4  38216  fmuldfeq  38650  stoweidlem43  38936  stoweidlem52  38945  stoweidlem53  38946  stoweidlem56  38949  issmfgt  39643  issmfge  39656  iccelpart  39971  fmtnoprmfac1  40015  fmtnoprmfac2  40017  pfxccat3a  40292  subgruhgredgd  40508  upgrwlkdvde  40943  crctcsh1wlkn0lem5  41017  crctcsh1wlkn0  41024  umgrwwlks2on  41161  rusgrnumwwlks  41177  rusgrnumwlkg  41180  3spthd  41343  av-numclwwlk5  41542  av-friendship  41553  copissgrp  41598  ringrng  41669  cznrng  41747  funcringcsetcALTV2lem9  41836  funcringcsetclem9ALTV  41859  linccl  41997  lincsumscmcl  42016  ldepsprlem  42055  lincresunit3lem1  42062