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

Theorem ibir 176
Description: Inference that converts a biconditional implied by one of its arguments, into an implication. (Contributed by NM, 22-Jul-2004.)
Hypothesis
Ref Expression
ibir.1  |-  ( ph  ->  ( ps  <->  ph ) )
Assertion
Ref Expression
ibir  |-  ( ph  ->  ps )

Proof of Theorem ibir
StepHypRef Expression
1 ibir.1 . . 3  |-  ( ph  ->  ( ps  <->  ph ) )
21bicomd 140 . 2  |-  ( ph  ->  ( ph  <->  ps )
)
32ibi 175 1  |-  ( 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:  pm5.21nii  678  elpr2  3519  eusv2i  4346  ffdm  5263  ov  5858  ovg  5877  nnacl  6344  elpm2r  6528  ltnqpri  7370  ltxrlt  7798  uzaddcl  9349  expcllem  10272  qexpclz  10282  1exp  10290  facnn  10441  fac0  10442  fac1  10443  bcn2  10478  znnen  11838
  Copyright terms: Public domain W3C validator