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  2766  cgsexg  2773  cgsex2g  2774  cgsex4g  2775  ceqsex  2776  spc2egv  2828  spc3egv  2830  csbiebt  3097  dfiin2g  3920  sotricim  4324  ralxfrALT  4468  iunpw  4481  opelxp  4657  ssrel  4715  ssrel2  4717  ssrelrel  4727  iss  4954  funcnvuni  5286  fun11iun  5483  tfrlem8  6319  eroveu  6626  fundmen  6806  nneneq  6857  fidifsnen  6870  prarloclem5  7499  prarloc  7502  recexprlemss1l  7634  recexprlemss1u  7635  uzin  9560  indstr  9593  elfzmlbp  10132
  Copyright terms: Public domain W3C validator