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

Theorem biimprcd 159
Description: Deduce a converse commuted implication from a logical equivalence. (Contributed by NM, 3-May-1994.) (Proof shortened by Wolf Lammen, 20-Dec-2013.)
Hypothesis
Ref Expression
biimpcd.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
biimprcd (𝜒 → (𝜑𝜓))

Proof of Theorem biimprcd
StepHypRef Expression
1 id 19 . 2 (𝜒𝜒)
2 biimpcd.1 . 2 (𝜑 → (𝜓𝜒))
31, 2syl5ibrcom 156 1 (𝜒 → (𝜑𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  biimparc  294  pm5.32  442  oplem1  922  ax11i  1650  equsex  1664  eleq1a  2160  ceqsalg  2650  cgsexg  2657  cgsex2g  2658  cgsex4g  2659  ceqsex  2660  spc2egv  2711  spc3egv  2713  csbiebt  2970  dfiin2g  3771  sotricim  4161  ralxfrALT  4304  iunpw  4317  opelxp  4483  ssrel  4541  ssrel2  4543  ssrelrel  4553  iss  4773  funcnvuni  5098  fun11iun  5289  tfrlem8  6099  eroveu  6399  fundmen  6579  nneneq  6629  fidifsnen  6642  prarloclem5  7122  prarloc  7125  recexprlemss1l  7257  recexprlemss1u  7258  uzin  9114  indstr  9144  elfzmlbp  9606
  Copyright terms: Public domain W3C validator