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

Theorem sylbir 125
Description: A mixed syllogism inference from a biconditional and an implication. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
sylbir.1 (ψφ)
sylbir.2 (ψχ)
Assertion
Ref Expression
sylbir (φχ)

Proof of Theorem sylbir
StepHypRef Expression
1 sylbir.1 . . 3 (ψφ)
21biimpri 124 . 2 (φψ)
3 sylbir.2 . 2 (ψχ)
42, 3syl 14 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  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  3imtr3i  189  3ori  1194  19.30dc  1515  nf4r  1558  cbvexh  1635  equveli  1639  sbequilem  1716  sb5rf  1729  nfsbxy  1815  nfsbxyt  1816  sbcomxyyz  1843  dvelimALT  1883  dvelimfv  1884  dvelimor  1891  mo2n  1925  mo23  1938  2exeu  1989  bm1.1  2022  necon1idc  2252  sbhypf  2597  vtocl2  2603  vtocl3  2604  reu6  2724  rmo2ilem  2841  uneqin  3182  abn0r  3237  inelcm  3276  vdif0im  3281  difrab0eqim  3282  r19.3rm  3304  r19.9rmv  3307  difprsn1  3494  intminss  3631  bm1.3ii  3869  intexabim  3897  copsex2g  3974  opelopabt  3990  eusv2nf  4154  reusv3i  4157  ordtri2orexmid  4211  setindel  4221  tfi  4248  mosubopt  4348  eqrelrel  4384  xpiindim  4416  opeliunxp2  4419  opelrn  4511  issref  4650  xpmlem  4687  rnxpid  4698  ssxpbm  4699  relcoi2  4791  unixpm  4796  cnviinm  4802  iotanul  4825  funimaexglem  4925  fvelrnb  5164  fvmptssdm  5198  fnfvrnss  5268  fressnfv  5293  fconstfvm  5322  f1mpt  5353  ovprc  5482  fo1stresm  5730  fo2ndresm  5731  reldmtpos  5809  tfrlem5  5871  tfrlem9  5876  tfri2  5893  ener  6195  domtr  6201  unen  6229  distrnqg  6371  nqnq0pi  6420  nqnq0a  6436  nqnq0m  6437  distrnq0  6441  nqprloc  6527  ltexprlemopl  6574  ltexprlemopu  6576  recexre  7342  nn1suc  7694  msqznn  8094  nn0ind  8108  fnn0ind  8110  ublbneg  8304  qreccl  8331  fzo1fzo0n0  8789  elfzom1elp1fzo  8808  fzo0end  8829  fzind2  8845  redivap  9082  imdivap  9089  sqrt0  9193  bdbm1.3ii  9325
  Copyright terms: Public domain W3C validator