Theorem adantld 273

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-1 5  ax-2 6  ax-mp 7  ax-ia2 106

This theorem is referenced by:  jaoa  676  dedlema  916  dedlemb  917  prlem1  920  equveli  1690  poxp  6011  nnmordi  6289  eroprf  6399  xpdom2  6601  elni2  6927  prarloclemlo  7107  xrlttr  9319  fzen  9511  eluzgtdifelfzo  9662  ssfzo12bi  9690  climuni  10735  mulcn2  10755  serf0  10795  dfgcd2  11335  lcmgcdlem  11391  lcmdvds  11393  qnumdencl  11497