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-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:  biimparc  297  pm5.32  450  oplem1  970  ax11i  1707  equsex  1721  eleq1a  2242  ceqsalg  2758  cgsexg  2765  cgsex2g  2766  cgsex4g  2767  ceqsex  2768  spc2egv  2820  spc3egv  2822  csbiebt  3088  dfiin2g  3906  sotricim  4308  ralxfrALT  4452  iunpw  4465  opelxp  4641  ssrel  4699  ssrel2  4701  ssrelrel  4711  iss  4937  funcnvuni  5267  fun11iun  5463  tfrlem8  6297  eroveu  6604  fundmen  6784  nneneq  6835  fidifsnen  6848  prarloclem5  7462  prarloc  7465  recexprlemss1l  7597  recexprlemss1u  7598  uzin  9519  indstr  9552  elfzmlbp  10088
  Copyright terms: Public domain W3C validator