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  3649  poxp  6392  nnmordi  6679  eroprf  6792  xpdom2  7010  elni2  7524  prarloclemlo  7704  xrlttr  10020  fzen  10268  eluzgtdifelfzo  10432  ssfzo12bi  10460  climuni  11844  mulcn2  11863  serf0  11903  ntrivcvgap  12099  dfgcd2  12575  lcmgcdlem  12639  lcmdvds  12641  qnumdencl  12749  infpnlem1  12922  cnplimcim  15381  dveflem  15440  gausslemma2dlem3  15782  uhgr2edg  16045  ushgredgedg  16065  ushgredgedgloop  16067  wlk1walkdom  16156  clwwlknun  16236  bj-charfundcALT  16340