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

Theorem biimpcd 152
Description: Deduce a commuted implication from a logical equivalence. (Contributed by NM, 3-May-1994.) (Proof shortened by Wolf Lammen, 22-Sep-2013.)
Hypothesis
Ref Expression
biimpcd.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
biimpcd  |-  ( ps 
->  ( ph  ->  ch ) )

Proof of Theorem biimpcd
StepHypRef Expression
1 id 19 . 2  |-  ( ps 
->  ps )
2 biimpcd.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2syl5ibcom 148 1  |-  ( ps 
->  ( ph  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  biimpac  286  3impexpbicom  1343  ax16  1710  ax16i  1754  nelneq  2154  nelneq2  2155  nelne1  2310  nelne2  2311  spc2gv  2660  spc3gv  2662  nssne1  3029  nssne2  3030  ifbothdc  3385  difsn  3529  iununir  3766  nbrne1  3809  nbrne2  3810  mosubopt  4433  issref  4735  ssimaex  5262  chfnrn  5306  ffnfv  5351  f1elima  5440  dftpos4  5909  snon0  6387  enq0sym  6588  prop  6631  prubl  6642  0fz1  9011  elfzmlbp  9092
  Copyright terms: Public domain W3C validator