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  619  elab3gf  2686  elpwi  3360  elpr2  3386  elpri  3387  elsni  3391  eltpi  3408  snssi  3499  prssi  3513  eloni  4078  limuni2  4100  elxpi  4304  releldmb  4514  relelrnb  4515  funeu  4869  fneu  4946  fvelima  5168  eloprabi  5764  fo2ndf  5790  tfrlem9  5876  ecexr  6047  elqsi  6094  qsel  6119  ecopovsym  6138  ecopovsymg  6141  brdomi  6166  en1uniel  6220  ltrnqi  6404  peano2nn  7667  eliooord  8527  fzrev3i  8680  elfzole1  8741  elfzolt2  8742  rere  9053
  Copyright terms: Public domain W3C validator