Theorem simpr2 969

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

Assertion

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

Proof of Theorem simpr2

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

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

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

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

This theorem is referenced by:  simplr2  1005  simprr2  1011  simp1r2  1059  simp2r2  1065  simp3r2  1071  3anandis  1306  isopolem  5675  tfrlemibacc  6175  tfrlemibfn  6177  tfr1onlembacc  6191  tfr1onlembfn  6193  tfrcllembacc  6204  tfrcllembfn  6206  prltlu  7237  prdisj  7242  prmuloc2  7317  ltntri  7807  eluzuzle  9230  xlesubadd  9553  elioc2  9606  elico2  9607  elicc2  9608  fseq1p1m1  9761  fz0fzelfz0  9791  seq3f1olemp  10162  bcval5  10396  hashdifpr  10453  summodclem2  11037  isumss2  11048  tanaddap  11291  dvds2ln  11368  divalglemeunn  11460  divalglemex  11461  divalglemeuneg  11462  isstructr  11811  restopnb  12187  icnpimaex  12216  cnptopresti  12243  psmettri  12313  isxmet2d  12331  xmettri  12355  metrtri  12360  xmetres2  12362  bldisj  12384  blss2ps  12389  blss2  12390  xmstri2  12453  mstri2  12454  xmstri  12455  mstri  12456  xmstri3  12457  mstri3  12458  msrtri  12459  comet  12482  bdbl  12486  xmetxp  12490  dvconst  12610