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  725  dedlema  975  dedlemb  976  prlem1  979  equveli  1805  ifnebibdc  3648  poxp  6376  nnmordi  6660  eroprf  6773  xpdom2  6986  elni2  7497  prarloclemlo  7677  xrlttr  9987  fzen  10235  eluzgtdifelfzo  10398  ssfzo12bi  10426  climuni  11799  mulcn2  11818  serf0  11858  ntrivcvgap  12054  dfgcd2  12530  lcmgcdlem  12594  lcmdvds  12596  qnumdencl  12704  infpnlem1  12877  cnplimcim  15335  dveflem  15394  gausslemma2dlem3  15736  uhgr2edg  15998  ushgredgedg  16018  ushgredgedgloop  16020  bj-charfundcALT  16130