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

Theorem biimprcd 160
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 157 1  |-  ( ch 
->  ( ph  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  biimparc  299  pm5.32  453  oplem1  975  ax11i  1714  equsex  1728  eleq1a  2249  ceqsalg  2765  cgsexg  2772  cgsex2g  2773  cgsex4g  2774  ceqsex  2775  spc2egv  2827  spc3egv  2829  csbiebt  3096  dfiin2g  3919  sotricim  4323  ralxfrALT  4467  iunpw  4480  opelxp  4656  ssrel  4714  ssrel2  4716  ssrelrel  4726  iss  4953  funcnvuni  5285  fun11iun  5482  tfrlem8  6318  eroveu  6625  fundmen  6805  nneneq  6856  fidifsnen  6869  prarloclem5  7498  prarloc  7501  recexprlemss1l  7633  recexprlemss1u  7634  uzin  9558  indstr  9591  elfzmlbp  10129
  Copyright terms: Public domain W3C validator