Theorem simpr3 1007

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

Assertion

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

Proof of Theorem simpr3

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

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

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 982

This theorem is referenced by:  simplr3  1043  simprr3  1049  simp1r3  1097  simp2r3  1103  simp3r3  1109  3anandis  1358  isopolem  5872  tfrlemibacc  6393  tfrlemibxssdm  6394  tfrlemibfn  6395  tfr1onlembacc  6409  tfr1onlembxssdm  6410  tfr1onlembfn  6411  tfrcllembacc  6422  tfrcllembxssdm  6423  tfrcllembfn  6424  elfir  7048  prloc  7577  prmuloc2  7653  ltntri  8173  eluzuzle  9628  xlesubadd  9977  elioc2  10030  elico2  10031  elicc2  10032  fseq1p1m1  10188  seq3f1olemp  10626  seq3f1oleml  10627  bcval5  10874  hashdifpr  10931  isumss2  11577  tanaddap  11923  dvds2ln  12008  divalglemeunn  12105  divalglemex  12106  divalglemeuneg  12107  f1ovscpbl  13016  prdssgrpd  13119  prdsmndd  13152  imasmnd2  13156  imasmnd  13157  grpsubadd  13292  grpaddsubass  13294  grpsubsub4  13297  grppnpcan2  13298  grpnpncan  13299  grpnnncan2  13301  imasgrp2  13318  imasgrp  13319  mulgnndir  13359  mulgnn0dir  13360  mulgnnass  13365  mulgnn0ass  13366  mulgass  13367  issubg2m  13397  qusgrp  13440  kerf1ghm  13482  cmn32  13512  cmn12  13514  abladdsub  13523  ablsubsub23  13533  rngass  13573  imasrng  13590  srgdilem  13603  srgass  13605  ringdilem  13646  ringass  13650  ringrng  13670  imasring  13698  opprrng  13711  opprring  13713  mulgass3  13719  unitgrp  13750  dvrass  13773  dvrdir  13777  subrgunit  13873  issubrg2  13875  aprap  13920  lss1  13996  lsssn0  14004  islss3  14013  sralmod  14084  restopnb  14525  icnpimaex  14555  cnptopresti  14582  psmettri  14674  isxmet2d  14692  xmettri  14716  metrtri  14721  xmetres2  14723  bldisj  14745  blss2ps  14750  blss2  14751  xmstri2  14814  mstri2  14815  xmstri  14816  mstri  14817  xmstri3  14818  mstri3  14819  msrtri  14820  comet  14843  bdbl  14847  xmetxp  14851  dvconst  15038  dvconstre  15040  dvconstss  15042  sgmmul  15340