Theorem anim2d 337

Description: Add a conjunct to left of antecedent and consequent in a deduction. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
anim1d.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
anim2d	⊢ (𝜑 → ((𝜃 ∧ 𝜓) → (𝜃 ∧ 𝜒)))

Proof of Theorem anim2d

Step	Hyp	Ref	Expression
1		idd 21	. 2 ⊢ (𝜑 → (𝜃 → 𝜃))
2		anim1d.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	anim12d 335	1 ⊢ (𝜑 → ((𝜃 ∧ 𝜓) → (𝜃 ∧ 𝜒)))

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  spsbim  1867  ssel  3188  sscon  3308  uniss  3873  trel3  4154  copsexg  4292  ssopab2  4326  coss1  4837  fununi  5347  imadif  5359  fss  5443  ssimaex  5647  opabbrex  5996  ssoprab2  6008  poxp  6325  pmss12g  6769  ss2ixp  6805  xpdom2  6933  qbtwnxr  10407  ioc0  10412  climshftlemg  11657  bezoutlembz  12369  tgcl  14580  neipsm  14670  ssnei2  14673  tgcnp  14725  cnpnei  14735  cnptopco  14738  mopni3  15000  limcresi  15182  cnlimcim  15187