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  1181  19.30dc  1500  nf4r  1543  cbvexh  1620  equveli  1624  sbequilem  1701  sb5rf  1714  nfsbxy  1800  nfsbxyt  1801  sbcomxyyz  1828  dvelimALT  1868  dvelimfv  1869  dvelimor  1876  mo2n  1910  mo23  1923  2exeu  1974  bm1.1  2007  necon1idc  2236  sbhypf  2580  vtocl2  2586  vtocl3  2587  reu6  2707  rmo2ilem  2824  uneqin  3165  abn0r  3220  inelcm  3259  vdif0im  3264  difrab0eqim  3265  r19.3rm  3289  r19.9rmv  3291  difprsn1  3477  intminss  3614  bm1.3ii  3852  intexabim  3880  copsex2g  3957  opelopabt  3973  eusv2nf  4138  reusv3i  4141  ordtri2orexmid  4195  setindel  4205  tfi  4232  mosubopt  4332  eqrelrel  4368  xpiindim  4400  opeliunxp2  4403  opelrn  4495  issref  4634  xpmlem  4671  rnxpid  4682  ssxpbm  4683  relcoi2  4775  unixpm  4780  cnviinm  4786  iotanul  4809  funimaexglem  4908  fvelrnb  5146  fvmptssdm  5180  fnfvrnss  5250  fressnfv  5275  fconstfvm  5304  f1mpt  5335  ovprc  5463  fo1stresm  5711  fo2ndresm  5712  reldmtpos  5790  tfrlem5  5852  tfrlem9  5857  tfri2  5874  distrnqg  6246  nqnq0pi  6293  nqnq0a  6309  nqnq0m  6310  distrnq0  6314  nqprloc  6400  ltexprlemopl  6438  ltexprlemopu  6440  bdbm1.3ii  7117
  Copyright terms: Public domain W3C validator