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 ⊢ (𝜑 → ((𝜃 ∧ 𝜓) → (𝜃 ∧ 𝜒)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  spsbim  1896  ssel  3242  sscon  3363  ifeqeqxdc  3687  uniss  3956  trel3  4237  copsexg  4384  ssopab2  4418  coss1  4935  fununi  5449  imadif  5461  fss  5546  ssimaex  5764  opabbrex  6132  ssoprab2  6144  poxp  6468  pmss12g  6956  ss2ixp  6993  xpdom2  7129  qbtwnxr  10694  ioc0  10699  climshftlemg  12070  bezoutlembz  12783  tgcl  15167  neipsm  15257  ssnei2  15260  tgcnp  15312  cnpnei  15322  cnptopco  15325  mopni3  15587  limcresi  15769  cnlimcim  15774