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

Theorem ibi 176
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 144 . 2  |-  ( ph  ->  ( ph  ->  ps ) )
32pm2.43i 49 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
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  ibir  177  pm5.21nii  704  elab3gf  2885  elpwi  3581  elsni  3607  elpr2  3611  elpri  3612  eltpi  3636  snssi  3733  prssi  3747  eloni  4369  limuni2  4391  elxpi  4636  releldmb  4857  relelrnb  4858  elrnmpt2d  4875  funeu  5233  fneu  5312  fvelima  5559  eloprabi  6187  fo2ndf  6218  tfrlem9  6310  ecexr  6530  elqsi  6577  qsel  6602  ecopovsym  6621  ecopovsymg  6624  elpmi  6657  elmapi  6660  pmsspw  6673  brdomi  6739  en1uniel  6794  mapdom1g  6837  dif1en  6869  enomnilem  7126  omnimkv  7144  mkvprop  7146  fodjumkvlemres  7147  enmkvlem  7149  enwomnilem  7157  ltrnqi  7395  peano2nnnn  7827  peano2nn  8902  eliooord  9897  fzrev3i  10056  elfzole1  10123  elfzolt2  10124  bcp1nk  10708  rere  10841  climcl  11257  climcau  11322  fprodcnv  11600  isstruct2im  12438  restsspw  12619  mgmcl  12643  submss  12728  subm0cl  12730  submcl  12731  istopfin  12991  uniopn  12992  iunopn  12993  inopn  12994  eltpsg  13031  basis1  13038  basis2  13039  eltg4i  13048  lmff  13242  psmetf  13318  psmet0  13320  psmettri2  13321  metflem  13342  xmetf  13343  xmeteq0  13352  xmettri2  13354  cncff  13557  cncfi  13558  limcresi  13628  dvcnp2cntop  13656  sinq34lt0t  13745  lgsdir2lem2  13923  2sqlem9  13953
  Copyright terms: Public domain W3C validator