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

Theorem anim2d 335
 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 333 1 (𝜑 → ((𝜃𝜓) → (𝜃𝜒)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  spsbim  1820  ssel  3118  sscon  3237  uniss  3789  trel3  4066  copsexg  4199  ssopab2  4230  coss1  4734  fununi  5231  imadif  5243  fss  5324  ssimaex  5522  opabbrex  5855  ssoprab2  5867  poxp  6169  pmss12g  6609  ss2ixp  6645  xpdom2  6765  qbtwnxr  10135  ioc0  10140  climshftlemg  11176  bezoutlembz  11859  tgcl  12403  neipsm  12493  ssnei2  12496  tgcnp  12548  cnpnei  12558  cnptopco  12561  mopni3  12823  limcresi  12974  cnlimcim  12979
 Copyright terms: Public domain W3C validator