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  721  dedlema  971  dedlemb  972  prlem1  975  equveli  1773  ifnebibdc  3605  poxp  6299  nnmordi  6583  eroprf  6696  xpdom2  6899  elni2  7398  prarloclemlo  7578  xrlttr  9887  fzen  10135  eluzgtdifelfzo  10290  ssfzo12bi  10318  climuni  11475  mulcn2  11494  serf0  11534  ntrivcvgap  11730  dfgcd2  12206  lcmgcdlem  12270  lcmdvds  12272  qnumdencl  12380  infpnlem1  12553  cnplimcim  14987  dveflem  15046  gausslemma2dlem3  15388  bj-charfundcALT  15539