Theorem adantld 278

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

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107

This theorem is referenced by:  jaoa  727  dedlema  977  dedlemb  978  prlem1  981  equveli  1807  ifnebibdc  3651  poxp  6396  nnmordi  6683  eroprf  6796  xpdom2  7014  elni2  7533  prarloclemlo  7713  xrlttr  10029  fzen  10277  eluzgtdifelfzo  10441  ssfzo12bi  10469  climuni  11853  mulcn2  11872  serf0  11912  ntrivcvgap  12108  dfgcd2  12584  lcmgcdlem  12648  lcmdvds  12650  qnumdencl  12758  infpnlem1  12931  cnplimcim  15390  dveflem  15449  gausslemma2dlem3  15791  uhgr2edg  16056  ushgredgedg  16076  ushgredgedgloop  16078  wlk1walkdom  16209  clwwlknun  16291  bj-charfundcALT  16404