Theorem adantld 272

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 108	. 2 ⊢ ((𝜃 ∧ 𝜓) → 𝜓)
2		adantld.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-ia2 105

This theorem is referenced by:  jaoa  673  dedlema  913  dedlemb  914  prlem1  917  equveli  1686  poxp  5954  nnmordi  6227  eroprf  6337  xpdom2  6499  elni2  6817  prarloclemlo  6997  xrlttr  9197  fzen  9389  eluzgtdifelfzo  9536  ssfzo12bi  9564  climuni  10576  mulcn2  10595  serif0  10633  dfgcd2  10885  lcmgcdlem  10941  lcmdvds  10943  qnumdencl  11047