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  721  dedlema  971  dedlemb  972  prlem1  975  equveli  1770  ifnebibdc  3600  poxp  6285  nnmordi  6569  eroprf  6682  xpdom2  6885  elni2  7374  prarloclemlo  7554  xrlttr  9861  fzen  10109  eluzgtdifelfzo  10264  ssfzo12bi  10292  climuni  11436  mulcn2  11455  serf0  11495  ntrivcvgap  11691  dfgcd2  12151  lcmgcdlem  12215  lcmdvds  12217  qnumdencl  12325  infpnlem1  12497  cnplimcim  14821  dveflem  14872  gausslemma2dlem3  15179  bj-charfundcALT  15301