ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  biimprcd Unicode 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  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
biimprcd  |-  ( ch 
->  ( ph  ->  ps ) )

Proof of Theorem biimprcd
StepHypRef Expression
1 id 19 . 2  |-  ( ch 
->  ch )
2 biimpcd.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2syl5ibrcom 156 1  |-  ( ch 
->  ( ph  ->  ps ) )
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  295  pm5.32  446  oplem1  942  ax11i  1675  equsex  1689  eleq1a  2187  ceqsalg  2686  cgsexg  2693  cgsex2g  2694  cgsex4g  2695  ceqsex  2696  spc2egv  2747  spc3egv  2749  csbiebt  3007  dfiin2g  3814  sotricim  4213  ralxfrALT  4356  iunpw  4369  opelxp  4537  ssrel  4595  ssrel2  4597  ssrelrel  4607  iss  4833  funcnvuni  5160  fun11iun  5354  tfrlem8  6181  eroveu  6486  fundmen  6666  nneneq  6717  fidifsnen  6730  prarloclem5  7272  prarloc  7275  recexprlemss1l  7407  recexprlemss1u  7408  uzin  9307  indstr  9337  elfzmlbp  9849
  Copyright terms: Public domain W3C validator