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

Theorem ibir 175
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 139 . 2  |-  ( ph  ->  ( ph  <->  ps )
)
32ibi 174 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  pm5.21nii  653  elpr2  3453  eusv2i  4253  ffdm  5147  ov  5723  ovg  5742  nnacl  6197  elpm2r  6377  ltnqpri  7100  ltxrlt  7499  uzaddcl  9009  expcllem  9868  qexpclz  9878  1exp  9886  facnn  10035  fac0  10036  fac1  10037  bcn2  10072  znnen  11117
  Copyright terms: Public domain W3C validator