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  4073  suctr  4343  fvun1  5487  opabbrex  5815  poxp  6129  tposfo2  6164  1idprl  7398  1idpru  7399  uzind  9162  xrlttr  9581  fzen  9823  fz0fzelfz0  9904  fisumss  11161  zeqzmulgcd  11659  lcmgcdlem  11758  lcmdvds  11760  cncongr2  11785  exprmfct  11818  metrest  12675  bj-om  13135