Theorem simpr2 988

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

Assertion

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

Proof of Theorem simpr2

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

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

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 964

This theorem is referenced by:  simplr2  1024  simprr2  1030  simp1r2  1078  simp2r2  1084  simp3r2  1090  3anandis  1325  isopolem  5716  tfrlemibacc  6216  tfrlemibfn  6218  tfr1onlembacc  6232  tfr1onlembfn  6234  tfrcllembacc  6245  tfrcllembfn  6247  prltlu  7288  prdisj  7293  prmuloc2  7368  ltntri  7883  eluzuzle  9327  xlesubadd  9659  elioc2  9712  elico2  9713  elicc2  9714  fseq1p1m1  9867  fz0fzelfz0  9897  seq3f1olemp  10268  bcval5  10502  hashdifpr  10559  summodclem2  11144  isumss2  11155  tanaddap  11435  dvds2ln  11515  divalglemeunn  11607  divalglemex  11608  divalglemeuneg  11609  isstructr  11963  restopnb  12339  icnpimaex  12369  cnptopresti  12396  psmettri  12488  isxmet2d  12506  xmettri  12530  metrtri  12535  xmetres2  12537  bldisj  12559  blss2ps  12564  blss2  12565  xmstri2  12628  mstri2  12629  xmstri  12630  mstri  12631  xmstri3  12632  mstri3  12633  msrtri  12634  comet  12657  bdbl  12661  xmetxp  12665  dvconst  12819