Theorem adantrd 273

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 107	. 2 ⊢ ((𝜓 ∧ 𝜃) → 𝜓)
2		adantrd.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	syl5 32	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜒))

Syntax hints:   → wi 4   ∧ wa 102

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

This theorem is referenced by:  syldan  276  jaoa  673  prlem1  915  equveli  1684  elssabg  3949  suctr  4212  fvun1  5315  opabbrex  5628  poxp  5932  tposfo2  5964  1idprl  7052  1idpru  7053  uzind  8753  xrlttr  9160  fzen  9352  fz0fzelfz0  9429  zeqzmulgcd  10742  lcmgcdlem  10839  lcmdvds  10841  cncongr2  10866  exprmfct  10899  bj-om  11175