ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  anim2d GIF version

Theorem anim2d 330
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
StepHypRef Expression
1 idd 21 . 2 (𝜑 → (𝜃𝜃))
2 anim1d.1 . 2 (𝜑 → (𝜓𝜒))
31, 2anim12d 328 1 (𝜑 → ((𝜃𝜓) → (𝜃𝜒)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  spsbim  1768  ssel  3008  sscon  3123  uniss  3657  trel3  3919  copsexg  4045  ssopab2  4076  coss1  4559  fununi  5047  imadif  5059  fss  5136  ssimaex  5328  opabbrex  5650  ssoprab2  5662  poxp  5954  pmss12g  6384  xpdom2  6499  qbtwnxr  9597  ioc0  9602  climshftlemg  10585  bezoutlembz  10875
  Copyright terms: Public domain W3C validator