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  1770  poxp  6258  nnmordi  6542  eroprf  6655  xpdom2  6858  elni2  7344  prarloclemlo  7524  xrlttr  9827  fzen  10075  eluzgtdifelfzo  10229  ssfzo12bi  10257  climuni  11336  mulcn2  11355  serf0  11395  ntrivcvgap  11591  dfgcd2  12050  lcmgcdlem  12112  lcmdvds  12114  qnumdencl  12222  infpnlem1  12394  cnplimcim  14613  dveflem  14664  bj-charfundcALT  15039