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

Theorem ibir 177
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 141 . 2  |-  ( ph  ->  ( ph  <->  ps )
)
32ibi 176 1  |-  ( 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:  pm5.21nii  704  elpr2  3613  eusv2i  4452  ffdm  5382  ov  5988  ovg  6007  nnacl  6475  elpm2r  6660  ltnqpri  7581  ltxrlt  8010  uzaddcl  9572  expcllem  10514  qexpclz  10524  1exp  10532  facnn  10688  fac0  10689  fac1  10690  bcn2  10725  znnen  12379
  Copyright terms: Public domain W3C validator