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  3604  poxp  6290  nnmordi  6574  eroprf  6687  xpdom2  6890  elni2  7381  prarloclemlo  7561  xrlttr  9870  fzen  10118  eluzgtdifelfzo  10273  ssfzo12bi  10301  climuni  11458  mulcn2  11477  serf0  11517  ntrivcvgap  11713  dfgcd2  12181  lcmgcdlem  12245  lcmdvds  12247  qnumdencl  12355  infpnlem1  12528  cnplimcim  14903  dveflem  14962  gausslemma2dlem3  15304  bj-charfundcALT  15455