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  640  prlem1  880  equveli  1642  elssabg  3902  suctr  4158  fvun1  5239  opabbrex  5549  poxp  5853  tposfo2  5882  1idprl  6688  1idpru  6689  uzind  8349  xrlttr  8716  fzen  8907  fz0fzelfz0  8984  bj-om  10061