Theorem simpr3 1029

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

Assertion

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

Proof of Theorem simpr3

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

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 1002

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 1004

This theorem is referenced by:  simplr3  1065  simprr3  1071  simp1r3  1119  simp2r3  1125  simp3r3  1131  3anandis  1381  isopolem  5955  tfrlemibacc  6483  tfrlemibxssdm  6484  tfrlemibfn  6485  tfr1onlembacc  6499  tfr1onlembxssdm  6500  tfr1onlembfn  6501  tfrcllembacc  6512  tfrcllembxssdm  6513  tfrcllembfn  6514  elfir  7156  prloc  7694  prmuloc2  7770  ltntri  8290  eluzuzle  9747  xlesubadd  10096  elioc2  10149  elico2  10150  elicc2  10151  fseq1p1m1  10307  seq3f1olemp  10754  seq3f1oleml  10755  bcval5  11002  hashdifpr  11060  ccatswrd  11223  pfxccat3a  11291  isumss2  11925  tanaddap  12271  dvds2ln  12356  divalglemeunn  12453  divalglemex  12454  divalglemeuneg  12455  f1ovscpbl  13366  prdssgrpd  13469  prdsmndd  13502  imasmnd2  13506  imasmnd  13507  grpsubadd  13642  grpaddsubass  13644  grpsubsub4  13647  grppnpcan2  13648  grpnpncan  13649  grpnnncan2  13651  imasgrp2  13668  imasgrp  13669  mulgnndir  13709  mulgnn0dir  13710  mulgnnass  13715  mulgnn0ass  13716  mulgass  13717  issubg2m  13747  qusgrp  13790  kerf1ghm  13832  cmn32  13862  cmn12  13864  abladdsub  13873  ablsubsub23  13883  rngass  13923  imasrng  13940  srgdilem  13953  srgass  13955  ringdilem  13996  ringass  14000  ringrng  14020  imasring  14048  opprrng  14061  opprring  14063  mulgass3  14069  unitgrp  14101  dvrass  14124  dvrdir  14128  subrgunit  14224  issubrg2  14226  aprap  14271  lss1  14347  lsssn0  14355  islss3  14364  sralmod  14435  restopnb  14876  icnpimaex  14906  cnptopresti  14933  psmettri  15025  isxmet2d  15043  xmettri  15067  metrtri  15072  xmetres2  15074  bldisj  15096  blss2ps  15101  blss2  15102  xmstri2  15165  mstri2  15166  xmstri  15167  mstri  15168  xmstri3  15169  mstri3  15170  msrtri  15171  comet  15194  bdbl  15198  xmetxp  15202  dvconst  15389  dvconstre  15391  dvconstss  15393  sgmmul  15691  pw1ndom3  16467