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  4502  evenodddisj  4517  spfininduct  4541  foco  5280  isocnv  5492  isores2  5494  f1oiso2  5501  fvfullfunlem3  5864  clos1induct  5881  weds  5939  ncspw1eu  6160  tlecg  6231  addccan2nc  6266  nchoicelem12  6301  fnfrec  6321