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  6566  1idpru  6567  uzind  8125  xrlttr  8486  fzen  8677  fz0fzelfz0  8754  bj-om  9396