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  7682  prarloclemlo  7862  xrlttr  10208  fzen  10458  eluzgtdifelfzo  10626  ssfzo12bi  10654  climuni  12077  mulcn2  12096  serf0  12136  ntrivcvgap  12333  dfgcd2  12809  lcmgcdlem  12873  lcmdvds  12875  qnumdencl  12985  infpnlem1  13160  prmlem1  13244  prmlem2  13256  rng1zrlem  14309  cnplimcim  15820  dveflem  15879  gausslemma2dlem3  16304  uhgr2edg  16569  ushgredgedg  16589  ushgredgedgloop  16591  wlk1walkdom  16722  clwwlknun  16804  bj-charfundcALT  16957