Theorem adantld 276

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 109	. 2 ⊢ ((𝜃 ∧ 𝜓) → 𝜓)
2		adantld.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	syl5 32	1 ⊢ (𝜑 → ((𝜃 ∧ 𝜓) → 𝜒))

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 106

This theorem is referenced by:  jaoa  710  dedlema  954  dedlemb  955  prlem1  958  equveli  1733  poxp  6137  nnmordi  6420  eroprf  6530  xpdom2  6733  elni2  7146  prarloclemlo  7326  xrlttr  9611  fzen  9854  eluzgtdifelfzo  10005  ssfzo12bi  10033  climuni  11094  mulcn2  11113  serf0  11153  ntrivcvgap  11349  dfgcd2  11738  lcmgcdlem  11794  lcmdvds  11796  qnumdencl  11901  cnplimcim  12844  dveflem  12895