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 ⊢ (𝜑 → ((𝜃 ∧ 𝜓) → 𝜒))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107

This theorem is used by:  jaoa  732  dedlema  982  dedlemb  983  prlem1  986  equveli  1812  ifnebibdc  3686  poxp  6468  ressuppss  6494  nnmordi  6789  eroprf  6902  xpdom2  7129  elni2  7681  prarloclemlo  7861  xrlttr  10207  fzen  10457  eluzgtdifelfzo  10625  ssfzo12bi  10653  climuni  12075  mulcn2  12094  serf0  12134  ntrivcvgap  12331  dfgcd2  12807  lcmgcdlem  12871  lcmdvds  12873  qnumdencl  12983  infpnlem1  13158  prmlem1  13242  prmlem2  13254  rng1zrlem  14307  cnplimcim  15817  dveflem  15876  gausslemma2dlem3  16280  uhgr2edg  16545  ushgredgedg  16565  ushgredgedgloop  16567  wlk1walkdom  16698  clwwlknun  16780  bj-charfundcALT  16933