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

Theorem ibi 165
 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 (𝜑 → (𝜑𝜓))
Assertion
Ref Expression
ibi (𝜑𝜓)

Proof of Theorem ibi
StepHypRef Expression
1 ibi.1 . . 3 (𝜑 → (𝜑𝜓))
21biimpd 132 . 2 (𝜑 → (𝜑𝜓))
32pm2.43i 43 1 (𝜑𝜓)
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 98 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  ibir  166  pm5.21nii  620  elab3gf  2692  elpwi  3368  elsni  3393  elpr2  3397  elpri  3398  eltpi  3417  snssi  3508  prssi  3522  eloni  4112  limuni2  4134  elxpi  4361  releldmb  4571  relelrnb  4572  funeu  4926  fneu  5003  fvelima  5225  eloprabi  5822  fo2ndf  5848  tfrlem9  5935  ecexr  6111  elqsi  6158  qsel  6183  ecopovsym  6202  ecopovsymg  6205  brdomi  6230  en1uniel  6284  dif1en  6337  ltrnqi  6519  peano2nnnn  6929  peano2nn  7926  eliooord  8797  fzrev3i  8950  elfzole1  9011  elfzolt2  9012  rere  9465  climcl  9803  climcau  9866
 Copyright terms: Public domain W3C validator