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  1766  ssel  3004  sscon  3118  uniss  3648  trel3  3909  copsexg  4035  ssopab2  4066  coss1  4549  fununi  5035  imadif  5047  fss  5123  ssimaex  5310  opabbrex  5628  ssoprab2  5640  poxp  5932  pmss12g  6362  xpdom2  6477  qbtwnxr  9558  ioc0  9563  climshftlemg  10515  bezoutlembz  10773
  Copyright terms: Public domain W3C validator