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  1807  ifnebibdc  3655  poxp  6406  ressuppss  6432  nnmordi  6727  eroprf  6840  xpdom2  7058  elni2  7577  prarloclemlo  7757  xrlttr  10074  fzen  10323  eluzgtdifelfzo  10488  ssfzo12bi  10516  climuni  11916  mulcn2  11935  serf0  11975  ntrivcvgap  12172  dfgcd2  12648  lcmgcdlem  12712  lcmdvds  12714  qnumdencl  12822  infpnlem1  12995  cnplimcim  15461  dveflem  15520  gausslemma2dlem3  15865  uhgr2edg  16130  ushgredgedg  16150  ushgredgedgloop  16152  wlk1walkdom  16283  clwwlknun  16365  bj-charfundcALT  16508