Theorem simpr2 989

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

Assertion

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

Proof of Theorem simpr2

Step	Hyp	Ref	Expression
1		simp2 983	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜒)
2	1	adantl 275	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 963

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

This theorem depends on definitions:  df-bi 116  df-3an 965

This theorem is referenced by:  simplr2  1025  simprr2  1031  simp1r2  1079  simp2r2  1085  simp3r2  1091  3anandis  1326  isopolem  5763  tfrlemibacc  6263  tfrlemibfn  6265  tfr1onlembacc  6279  tfr1onlembfn  6281  tfrcllembacc  6292  tfrcllembfn  6294  prltlu  7386  prdisj  7391  prmuloc2  7466  ltntri  7982  eluzuzle  9426  xlesubadd  9765  elioc2  9818  elico2  9819  elicc2  9820  fseq1p1m1  9974  fz0fzelfz0  10004  seq3f1olemp  10379  bcval5  10614  hashdifpr  10671  summodclem2  11256  isumss2  11267  tanaddap  11613  dvds2ln  11693  divalglemeunn  11785  divalglemex  11786  divalglemeuneg  11787  isstructr  12152  restopnb  12528  icnpimaex  12558  cnptopresti  12585  psmettri  12677  isxmet2d  12695  xmettri  12719  metrtri  12724  xmetres2  12726  bldisj  12748  blss2ps  12753  blss2  12754  xmstri2  12817  mstri2  12818  xmstri  12819  mstri  12820  xmstri3  12821  mstri3  12822  msrtri  12823  comet  12846  bdbl  12850  xmetxp  12854  dvconst  13008