Theorem adantrd 264

Description: Deduction adding a conjunct to the right of an antecedent. (Contributed by NM, 4-May-1994.)

Hypothesis

Ref	Expression
adantrd.1	⊢ (φ → (ψ → χ))

Assertion

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

Proof of Theorem adantrd

Step	Hyp	Ref	Expression
1		simpl 102	. 2 ⊢ ((ψ ∧ θ) → ψ)
2		adantrd.1	. 2 ⊢ (φ → (ψ → χ))
3	1, 2	syl5 28	1 ⊢ (φ → ((ψ ∧ θ) → χ))

Syntax hints:   → wi 4   ∧ wa 97

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99

This theorem is referenced by:  syldan  266  jaoa  639  prlem1  879  equveli  1639  elssabg  3893  suctr  4124  fvun1  5182  opabbrex  5491  poxp  5794  tposfo2  5823  1idprl  6565  1idpru  6566  uzind  8105  xrlttr  8466  fzen  8657  fz0fzelfz0  8734  bj-om  9371