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  728  dedlema  978  dedlemb  979  prlem1  982  equveli  1808  ifnebibdc  3668  poxp  6428  ressuppss  6454  nnmordi  6749  eroprf  6862  xpdom2  7082  elni2  7629  prarloclemlo  7809  xrlttr  10128  fzen  10377  eluzgtdifelfzo  10542  ssfzo12bi  10570  climuni  11978  mulcn2  11997  serf0  12037  ntrivcvgap  12234  dfgcd2  12710  lcmgcdlem  12774  lcmdvds  12776  qnumdencl  12884  infpnlem1  13057  cnplimcim  15532  dveflem  15591  gausslemma2dlem3  15936  uhgr2edg  16201  ushgredgedg  16221  ushgredgedgloop  16223  wlk1walkdom  16354  clwwlknun  16436  bj-charfundcALT  16579