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  725  dedlema  975  dedlemb  976  prlem1  979  equveli  1805  ifnebibdc  3648  poxp  6384  nnmordi  6670  eroprf  6783  xpdom2  6998  elni2  7512  prarloclemlo  7692  xrlttr  10003  fzen  10251  eluzgtdifelfzo  10415  ssfzo12bi  10443  climuni  11819  mulcn2  11838  serf0  11878  ntrivcvgap  12074  dfgcd2  12550  lcmgcdlem  12614  lcmdvds  12616  qnumdencl  12724  infpnlem1  12897  cnplimcim  15356  dveflem  15415  gausslemma2dlem3  15757  uhgr2edg  16019  ushgredgedg  16039  ushgredgedgloop  16041  wlk1walkdom  16100  bj-charfundcALT  16227