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

Theorem biimprcd 158
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 155 1  |-  ( ch 
->  ( ph  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  biimparc  293  pm5.32  441  oplem1  917  ax11i  1643  equsex  1657  eleq1a  2151  ceqsalg  2628  cgsexg  2635  cgsex2g  2636  cgsex4g  2637  ceqsex  2638  spc2egv  2688  spc3egv  2690  csbiebt  2943  dfiin2g  3719  sotricim  4086  ralxfrALT  4225  iunpw  4237  opelxp  4400  ssrel  4454  ssrel2  4456  ssrelrel  4466  iss  4684  funcnvuni  4999  fun11iun  5178  tfrlem8  5967  eroveu  6263  fundmen  6353  nneneq  6392  fidifsnen  6405  prarloclem5  6752  prarloc  6755  recexprlemss1l  6887  recexprlemss1u  6888  uzin  8732  indstr  8762  elfzmlbp  9220
  Copyright terms: Public domain W3C validator