Theorem adantrd 277

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

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  syldan  280  jaoa  709  prlem1  957  equveli  1732  elssabg  4068  suctr  4338  fvun1  5480  opabbrex  5808  poxp  6122  tposfo2  6157  1idprl  7391  1idpru  7392  uzind  9155  xrlttr  9574  fzen  9816  fz0fzelfz0  9897  fisumss  11154  zeqzmulgcd  11648  lcmgcdlem  11747  lcmdvds  11749  cncongr2  11774  exprmfct  11807  metrest  12664  bj-om  13124