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  727  dedlema  977  dedlemb  978  prlem1  981  equveli  1807  ifnebibdc  3651  poxp  6397  nnmordi  6684  eroprf  6797  xpdom2  7015  elni2  7534  prarloclemlo  7714  xrlttr  10030  fzen  10278  eluzgtdifelfzo  10443  ssfzo12bi  10471  climuni  11871  mulcn2  11890  serf0  11930  ntrivcvgap  12127  dfgcd2  12603  lcmgcdlem  12667  lcmdvds  12669  qnumdencl  12777  infpnlem1  12950  cnplimcim  15410  dveflem  15469  gausslemma2dlem3  15811  uhgr2edg  16076  ushgredgedg  16096  ushgredgedgloop  16098  wlk1walkdom  16229  clwwlknun  16311  bj-charfundcALT  16455