ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ibi Structured version   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  607  elab3gf  2669  elpwi  3343  elpr2  3369  elpri  3370  elsni  3374  eltpi  3391  snssi  3482  prssi  3496  eloni  4061  limuni2  4083  elxpi  4288  releldmb  4498  relelrnb  4499  funeu  4852  fneu  4929  fvelima  5150  eloprabi  5745  fo2ndf  5771  tfrlem9  5857  ecexr  6022  elqsi  6069  qsel  6094  ecopovsym  6113  ecopovsymg  6116  ltbtwnnqq  6272  ltrnqi  6278
  Copyright terms: Public domain W3C validator