Theorem adantrr 697

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)

Hypothesis

Ref	Expression
adant2.1	⊢ ((φ ∧ ψ) → χ)

Assertion

Ref	Expression
adantrr	⊢ ((φ ∧ (ψ ∧ θ)) → χ)

Proof of Theorem adantrr

Step	Hyp	Ref	Expression
1		simpl 443	. 2 ⊢ ((ψ ∧ θ) → ψ)
2		adant2.1	. 2 ⊢ ((φ ∧ ψ) → χ)
3	1, 2	sylan2 460	1 ⊢ ((φ ∧ (ψ ∧ θ)) → χ)

Syntax hints:   → wi 4   ∧ wa 358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  ad2ant2r  727  ad2ant2lr  728  consensus  925  3ad2antr1  1120  sbcom  2089  ax11eq  2193  ax11el  2194  nndisjeq  4429  tfinpw1  4494  tfinsuc  4498  sfindbl  4530  vfinspsslem1  4550  isocnv  5491  isores2  5493  isoini  5497  f1oiso2  5500  ncspw1eu  6159  addccan2nc  6265  frecxp  6314  fnfrec  6320