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  722  dedlema  972  dedlemb  973  prlem1  976  equveli  1783  ifnebibdc  3620  poxp  6331  nnmordi  6615  eroprf  6728  xpdom2  6941  elni2  7447  prarloclemlo  7627  xrlttr  9937  fzen  10185  eluzgtdifelfzo  10348  ssfzo12bi  10376  climuni  11679  mulcn2  11698  serf0  11738  ntrivcvgap  11934  dfgcd2  12410  lcmgcdlem  12474  lcmdvds  12476  qnumdencl  12584  infpnlem1  12757  cnplimcim  15214  dveflem  15273  gausslemma2dlem3  15615  bj-charfundcALT  15883