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

Theorem anim2d 320
 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 318 1 (𝜑 → ((𝜃𝜓) → (𝜃𝜒)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  spsbim  1724  ssel  2939  sscon  3077  uniss  3601  trel3  3862  copsexg  3981  ssopab2  4012  coss1  4491  fununi  4967  imadif  4979  fss  5054  ssimaex  5234  opabbrex  5549  ssoprab2  5561  poxp  5853  xpdom2  6305  climshftlemg  9823
 Copyright terms: Public domain W3C validator