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

Theorem sylbir 129
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 128 . 2 (𝜑𝜓)
3 sylbir.2 . 2 (𝜓𝜒)
42, 3syl 14 1 (𝜑𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  3imtr3i  193  3ori  1206  19.30dc  1534  nf4r  1577  cbvexh  1654  equveli  1658  sbequilem  1735  sb5rf  1748  nfsbxy  1834  nfsbxyt  1835  sbcomxyyz  1862  dvelimALT  1902  dvelimfv  1903  dvelimor  1910  mo2n  1944  mo23  1957  2exeu  2008  bm1.1  2041  necon1idc  2273  sbhypf  2620  vtocl2  2626  vtocl3  2627  reu6  2753  rmo2ilem  2875  uneqin  3216  abn0r  3271  inelcm  3310  vdif0im  3315  difrab0eqim  3316  r19.3rm  3338  r19.9rmv  3341  difprsn1  3531  intminss  3668  bm1.3ii  3906  intexabim  3934  copsex2g  4011  opelopabt  4027  eusv2nf  4216  reusv3i  4219  onintrab2im  4272  ordtri2orexmid  4276  setindel  4291  onsucuni2  4316  ordtri2or2exmid  4324  zfregfr  4326  tfi  4333  mosubopt  4433  eqrelrel  4469  xpiindim  4501  opeliunxp2  4504  opelrn  4596  issref  4735  xpmlem  4772  rnxpid  4783  ssxpbm  4784  relcoi2  4876  unixpm  4881  cnviinm  4887  iotanul  4910  funimaexglem  5010  fvelrnb  5249  fvmptssdm  5283  fnfvrnss  5353  fressnfv  5378  fconstfvm  5407  f1mpt  5438  ovprc  5568  fo1stresm  5816  fo2ndresm  5817  spc2ed  5882  reldmtpos  5899  tfrlem5  5961  tfrlem9  5966  tfri2  5983  ener  6290  domtr  6296  unen  6324  cardval3ex  6423  distrnqg  6543  nqnq0pi  6594  nqnq0a  6610  nqnq0m  6611  distrnq0  6615  nqprloc  6701  ltexprlemopl  6757  ltexprlemopu  6759  recexre  7643  nn1suc  8009  msqznn  8397  nn0ind  8411  fnn0ind  8413  ublbneg  8645  qreccl  8674  fzo1fzo0n0  9141  elfzom1elp1fzo  9160  fzo0end  9181  fzind2  9197  flqeqceilz  9268  iser0f  9416  redivap  9702  imdivap  9709  cvg1nlemres  9812  sqrt0  9831  odd2np1  10184  opoe  10207  omoe  10208  opeo  10209  omeo  10210  ialgfx  10274  bdbm1.3ii  10398
  Copyright terms: Public domain W3C validator