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

Theorem biimprcd 149
 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 146 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 98 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:  biimparc  283  pm5.32  426  oplem1  882  ax11i  1602  equsex  1616  eleq1a  2109  ceqsalg  2582  cgsexg  2589  cgsex2g  2590  cgsex4g  2591  ceqsex  2592  spc2egv  2642  spc3egv  2644  csbiebt  2886  dfiin2g  3690  sotricim  4060  ralxfrALT  4199  iunpw  4211  opelxp  4374  ssrel  4428  ssrel2  4430  ssrelrel  4440  iss  4654  funcnvuni  4968  fun11iun  5147  tfrlem8  5934  eroveu  6197  fundmen  6286  nneneq  6320  fidifsnen  6331  prarloclem5  6598  prarloc  6601  recexprlemss1l  6733  recexprlemss1u  6734  uzin  8505  indstr  8536  elfzmlbp  8990
 Copyright terms: Public domain W3C validator