Theorem simpr3 1005

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

Assertion

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

Proof of Theorem simpr3

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

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

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 980

This theorem is referenced by:  simplr3  1041  simprr3  1047  simp1r3  1095  simp2r3  1101  simp3r3  1107  3anandis  1347  isopolem  5823  tfrlemibacc  6327  tfrlemibxssdm  6328  tfrlemibfn  6329  tfr1onlembacc  6343  tfr1onlembxssdm  6344  tfr1onlembfn  6345  tfrcllembacc  6356  tfrcllembxssdm  6357  tfrcllembfn  6358  elfir  6972  prloc  7490  prmuloc2  7566  ltntri  8085  eluzuzle  9536  xlesubadd  9883  elioc2  9936  elico2  9937  elicc2  9938  fseq1p1m1  10094  seq3f1olemp  10502  seq3f1oleml  10503  bcval5  10743  hashdifpr  10800  isumss2  11401  tanaddap  11747  dvds2ln  11831  divalglemeunn  11926  divalglemex  11927  divalglemeuneg  11928  f1ovscpbl  12733  grpsubadd  12958  grpaddsubass  12960  grpsubsub4  12963  grppnpcan2  12964  grpnpncan  12965  grpnnncan2  12967  mulgnndir  13012  mulgnn0dir  13013  mulgnnass  13018  mulgnn0ass  13019  mulgass  13020  issubg2m  13049  cmn32  13107  cmn12  13109  abladdsub  13118  ablsubsub23  13128  srgdilem  13152  srgass  13154  ringdilem  13195  ringass  13199  opprring  13249  mulgass3  13254  unitgrp  13285  dvrass  13308  dvrdir  13312  subrgunit  13360  issubrg2  13362  aprap  13376  restopnb  13684  icnpimaex  13714  cnptopresti  13741  psmettri  13833  isxmet2d  13851  xmettri  13875  metrtri  13880  xmetres2  13882  bldisj  13904  blss2ps  13909  blss2  13910  xmstri2  13973  mstri2  13974  xmstri  13975  mstri  13976  xmstri3  13977  mstri3  13978  msrtri  13979  comet  14002  bdbl  14006  xmetxp  14010  dvconst  14164