Theorem adantld 276

Description: Deduction adding a conjunct to the left of an antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 20-Dec-2012.)

Hypothesis

Ref	Expression
adantld.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
adantld	⊢ (𝜑 → ((𝜃 ∧ 𝜓) → 𝜒))

Proof of Theorem adantld

Step	Hyp	Ref	Expression
1		simpr 109	. 2 ⊢ ((𝜃 ∧ 𝜓) → 𝜓)
2		adantld.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-ia2 106

This theorem is referenced by:  jaoa  709  dedlema  953  dedlemb  954  prlem1  957  equveli  1732  poxp  6129  nnmordi  6412  eroprf  6522  xpdom2  6725  elni2  7129  prarloclemlo  7309  xrlttr  9588  fzen  9830  eluzgtdifelfzo  9981  ssfzo12bi  10009  climuni  11069  mulcn2  11088  serf0  11128  ntrivcvgap  11324  dfgcd2  11709  lcmgcdlem  11765  lcmdvds  11767  qnumdencl  11872  cnplimcim  12815  dveflem  12865