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  10442  ssfzo12bi  10470  climuni  11854  mulcn2  11873  serf0  11913  ntrivcvgap  12110  dfgcd2  12586  lcmgcdlem  12650  lcmdvds  12652  qnumdencl  12760  infpnlem1  12933  cnplimcim  15393  dveflem  15452  gausslemma2dlem3  15794  uhgr2edg  16059  ushgredgedg  16079  ushgredgedgloop  16081  wlk1walkdom  16212  clwwlknun  16294  bj-charfundcALT  16407