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  3493  intminss  3630  bm1.3ii  3868  intexabim  3896  copsex2g  3973  opelopabt  3989  eusv2nf  4153  reusv3i  4156  ordtri2orexmid  4210  setindel  4220  tfi  4247  mosubopt  4347  eqrelrel  4383  xpiindim  4415  opeliunxp2  4418  opelrn  4510  issref  4649  xpmlem  4686  rnxpid  4697  ssxpbm  4698  relcoi2  4790  unixpm  4795  cnviinm  4801  iotanul  4824  funimaexglem  4923  fvelrnb  5162  fvmptssdm  5196  fnfvrnss  5266  fressnfv  5291  fconstfvm  5320  f1mpt  5351  ovprc  5479  fo1stresm  5727  fo2ndresm  5728  reldmtpos  5806  tfrlem5  5868  tfrlem9  5873  tfri2  5890  ener  6188  domtr  6194  unen  6222  distrnqg  6364  nqnq0pi  6413  nqnq0a  6429  nqnq0m  6430  distrnq0  6434  nqprloc  6521  ltexprlemopl  6565  ltexprlemopu  6567  recexre  7314  nn1suc  7665  msqznn  8063  nn0ind  8077  fnn0ind  8079  ublbneg  8273  qreccl  8300  fzo1fzo0n0  8755  elfzom1elp1fzo  8774  fzo0end  8795  fzind2  8811  bdbm1.3ii  8944
  Copyright terms: Public domain W3C validator