Theorem adantrl 696

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
adantrl	⊢ ((φ ∧ (θ ∧ ψ)) → χ)

Proof of Theorem adantrl

Step	Hyp	Ref	Expression
1		simpr 447	. 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:  ad2ant2l  726  ad2ant2rl  729  consensus  925  3ad2antr2  1121  3ad2antr3  1122  sbcom  2089  tfinltfin  4501  evenodddisj  4516  spfininduct  4540  foco  5279  isocnv  5491  isores2  5493  f1oiso2  5500  fvfullfunlem3  5863  clos1induct  5880  weds  5938  ncspw1eu  6159  tlecg  6230  addccan2nc  6265  nchoicelem12  6300  fnfrec  6320