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  7400  prarloclemlo  7580  xrlttr  9889  fzen  10137  eluzgtdifelfzo  10292  ssfzo12bi  10320  climuni  11477  mulcn2  11496  serf0  11536  ntrivcvgap  11732  dfgcd2  12208  lcmgcdlem  12272  lcmdvds  12274  qnumdencl  12382  infpnlem1  12555  cnplimcim  15011  dveflem  15070  gausslemma2dlem3  15412  bj-charfundcALT  15563