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

Theorem ibi 169
 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 136 . 2 (𝜑 → (𝜑𝜓))
32pm2.43i 47 1 (𝜑𝜓)
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 102 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103 This theorem depends on definitions:  df-bi 114 This theorem is referenced by:  ibir  170  pm5.21nii  630  elab3gf  2715  elpwi  3396  elsni  3421  elpr2  3425  elpri  3426  eltpi  3445  snssi  3536  prssi  3550  eloni  4140  limuni2  4162  elxpi  4389  releldmb  4599  relelrnb  4600  funeu  4954  fneu  5031  fvelima  5253  eloprabi  5850  fo2ndf  5876  tfrlem9  5966  ecexr  6142  elqsi  6189  qsel  6214  ecopovsym  6233  ecopovsymg  6236  brdomi  6261  en1uniel  6315  dif1en  6368  ltrnqi  6577  peano2nnnn  6987  peano2nn  8002  eliooord  8898  fzrev3i  9052  elfzole1  9113  elfzolt2  9114  bcp1nk  9630  rere  9693  climcl  10034  climcau  10097
 Copyright terms: Public domain W3C validator