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

Theorem ibi 174
Description: Inference that converts a biconditional implied by one of its arguments, into an implication. (Contributed by NM, 17-Oct-2003.)
Hypothesis
Ref Expression
ibi.1  |-  ( ph  ->  ( ph  <->  ps )
)
Assertion
Ref Expression
ibi  |-  ( ph  ->  ps )

Proof of Theorem ibi
StepHypRef Expression
1 ibi.1 . . 3  |-  ( ph  ->  ( ph  <->  ps )
)
21biimpd 142 . 2  |-  ( ph  ->  ( ph  ->  ps ) )
32pm2.43i 48 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
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  ibir  175  pm5.21nii  653  elab3gf  2744  elpwi  3393  elsni  3418  elpr2  3422  elpri  3423  eltpi  3441  snssi  3531  prssi  3545  eloni  4132  limuni2  4154  elxpi  4381  releldmb  4593  relelrnb  4594  funeu  4950  fneu  5028  fvelima  5251  eloprabi  5847  fo2ndf  5873  tfrlem9  5962  ecexr  6170  elqsi  6217  qsel  6242  ecopovsym  6261  ecopovsymg  6264  brdomi  6289  en1uniel  6343  dif1en  6404  ltrnqi  6662  peano2nnnn  7072  peano2nn  8107  eliooord  9016  fzrev3i  9170  elfzole1  9230  elfzolt2  9231  bcp1nk  9775  rere  9879  climcl  10248  climcau  10311
  Copyright terms: Public domain W3C validator