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

Theorem sylbir 134
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 132 . 2 (𝜑𝜓)
3 sylbir.2 . 2 (𝜓𝜒)
42, 3syl 14 1 (𝜑𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  3imtr3i  199  3ori  1279  19.30dc  1607  nf4r  1650  cbvexh  1729  equveli  1733  sbequilem  1811  sb5rf  1825  nfsbxy  1916  nfsbxyt  1917  sbcomxyyz  1946  dvelimALT  1986  dvelimfv  1987  dvelimor  1994  mo2n  2028  mo23  2041  2exeu  2092  bm1.1  2125  necon1idc  2362  sbhypf  2736  vtocl2  2742  vtocl3  2743  reu6  2874  rmo2ilem  2999  uneqin  3328  abn0r  3388  inelcm  3424  vdif0im  3429  difrab0eqim  3430  r19.3rm  3452  r19.9rmv  3455  difprsn1  3663  intminss  3800  disjnim  3924  bm1.3ii  4053  intexabim  4081  copsex2g  4172  opelopabt  4188  eusv2nf  4381  reusv3i  4384  onintrab2im  4438  ordtri2orexmid  4442  setindel  4457  onsucuni2  4483  ordtri2or2exmid  4490  zfregfr  4492  tfi  4500  mosubopt  4608  eqrelrel  4644  xpiindim  4680  opeliunxp2  4683  opelrn  4777  issref  4925  xpmlem  4963  rnxpid  4977  ssxpbm  4978  relcoi2  5073  unixpm  5078  cnviinm  5084  iotanul  5107  funimaexglem  5210  fvelrnb  5473  fvmptssdm  5509  fnfvrnss  5584  fressnfv  5611  fconstfvm  5642  f1mpt  5676  ovprc  5810  fo1stresm  6063  fo2ndresm  6064  spc2ed  6134  opeliunxp2f  6139  reldmtpos  6154  tfrlem5  6215  tfrlem9  6220  tfri2  6267  frecfcllem  6305  frecsuclem  6307  fvmptmap  6583  ixpiinm  6622  ixp0  6629  mptelixpg  6632  ener  6677  domtr  6683  unen  6714  xpf1o  6742  mapen  6744  cardval3ex  7054  distrnqg  7215  nqnq0pi  7266  nqnq0a  7282  nqnq0m  7283  distrnq0  7287  nqprloc  7373  ltexprlemopl  7429  ltexprlemopu  7431  recexre  8360  nn1suc  8759  msqznn  9171  nn0ind  9185  fnn0ind  9187  ublbneg  9428  qreccl  9457  fzo1fzo0n0  9987  elfzom1elp1fzo  10006  fzo0end  10027  fzind2  10043  flqeqceilz  10118  nnsinds  10243  nn0sinds  10244  ser0f  10315  hashfacen  10607  redivap  10674  imdivap  10681  cvg1nlemres  10785  sqrt0  10804  summodclem3  11177  fsump1i  11230  prodf1  11339  cos1bnd  11493  odd2np1  11597  opoe  11619  omoe  11620  opeo  11621  omeo  11622  dfgcd2  11729  gcdmultiplez  11736  dvdssq  11746  algfx  11760  setsfun0  12025  neipsm  12353  txbas  12457  elcncf1di  12765  reeff1o  12893  sincosq1lem  12945  sincosq2sgn  12947  sincosq4sgn  12949  bdbm1.3ii  13243
  Copyright terms: Public domain W3C validator