Theorem adantld 272

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 108	. 2 ⊢ ((𝜃 ∧ 𝜓) → 𝜓)
2		adantld.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	syl5 32	1 ⊢ (𝜑 → ((𝜃 ∧ 𝜓) → 𝜒))

Syntax hints:   → wi 4   ∧ wa 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 105

This theorem is referenced by:  jaoa  672  dedlema  910  dedlemb  911  prlem1  914  equveli  1682  poxp  5873  nnmordi  6112  eroprf  6222  xpdom2  6328  elni2  6504  prarloclemlo  6684  xrlttr  8870  fzen  9062  eluzgtdifelfzo  9206  ssfzo12bi  9234  climuni  10132  mulcn2  10151  serif0  10189  dfgcd2  10403  lcmgcdlem  10459  lcmdvds  10461