New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  ibi GIF version

Theorem ibi 232
 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 198 . 2 (φ → (φψ))
32pm2.43i 43 1 (φψ)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 176 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8 This theorem depends on definitions:  df-bi 177 This theorem is referenced by:  ibir  233  elimh  922  elab3gf  2990  elimhyp  3710  elimhyp2v  3711  elimhyp3v  3712  elimhyp4v  3713  elpwi  3730  elpr2  3752  elpri  3753  elsni  3757  eltpi  3770  snssi  3852  prssi  3863  evennn  4506  oddnn  4507  evennnul  4508  oddnnul  4509  sucevenodd  4510  sucoddeven  4511  eventfin  4517  oddtfin  4518  nnadjoin  4520  nnadjoinpw  4521  elxpi  4800  elfunsi  5831  trd  5921  frd  5922  extd  5923  symd  5924  refd  5927  antid  5929  connexd  5931  elqsi  5978  pmfun  6015  elmapi  6016  cannc  6333  cantc  6336
 Copyright terms: Public domain W3C validator