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

Theorem sylanbrc 394
Description: Syllogism inference. (Contributed by Jeff Madsen, 2-Sep-2009.)
Hypotheses
Ref Expression
sylanbrc.1 (φψ)
sylanbrc.2 (φχ)
sylanbrc.3 (θ ↔ (ψ χ))
Assertion
Ref Expression
sylanbrc (φθ)

Proof of Theorem sylanbrc
StepHypRef Expression
1 sylanbrc.1 . . 3 (φψ)
2 sylanbrc.2 . . 3 (φχ)
31, 2jca 290 . 2 (φ → (ψ χ))
4 sylanbrc.3 . 2 (θ ↔ (ψ χ))
53, 4sylibr 137 1 (φθ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  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:  sb2  1647  sbequ1  1648  sbidm  1728  eqeu  2705  euind  2722  reuind  2738  eldifd  2922  eqssd  2956  ssrabdv  3013  psstr  3043  sspsstr  3044  psssstr  3045  opm  3962  issod  4047  ordsucim  4192  en2lp  4232  sosng  4356  sotri2  4665  sotri3  4666  relssdmrn  4784  funun  4887  fnsng  4890  fnprg  4897  fntpg  4898  fntp  4899  fununi  4910  imain  4924  fnco  4950  f00  5024  f1ss  5040  f1ssr  5041  f1ssres  5042  f1f1orn  5080  foimacnv  5087  foun  5088  fun11iun  5090  sefvex  5139  dff3im  5255  foco2  5261  fmpt  5262  ffnfv  5266  fmpt2d  5270  ffvresb  5271  fprg  5289  fcof1  5366  fcofo  5367  fcof1o  5372  fliftf  5382  isoini2  5401  f1oiso  5408  moriotass  5439  fnoprabg  5544  f1ocnvd  5644  suppssfv  5650  suppssov1  5651  1stcof  5732  2ndcof  5733  1stconst  5784  2ndconst  5785  fo2ndf  5790  f1o2ndf1  5791  smores2  5850  tfrlem5  5871  tfrlemibfn  5883  nntri2  6012  eroveu  6133  dom2lem  6188  addclpi  6311  mulclpi  6312  nnppipi  6327  recmulnqg  6375  enq0ref  6415  nqnq0pi  6420  genipv  6491  addclpr  6519  nqprxx  6528  prmuloc  6546  mulclpr  6552  distrlem1prl  6557  distrlem1pru  6558  ltexprlempr  6581  ltexprlemrl  6583  ltexprlemru  6585  recexprlempr  6603  cauappcvgprlemm  6616  cauappcvgprlemopl  6617  cauappcvgprlemlol  6618  cauappcvgprlemopu  6619  cauappcvgprlemupu  6620  cauappcvgprlemloc  6623  cauappcvgprlemcl  6624  cauappcvgprlemladdfu  6625  cauappcvgprlemladdfl  6626  cauappcvgprlem2  6631  receuap  7412  divvalap  7415  cju  7674  nn0ge2m1nn  7998  nnnegz  8004  elnnz  8011  elnn0z  8014  peano2z  8037  nn0n0n1ge2  8067  msqznn  8094  eluzaddi  8255  eluzsubi  8256  uzind4  8287  elnn1uz2  8300  uz2mulcl  8301  divfnzn  8312  nnrp  8347  rpaddcl  8361  rpmulcl  8362  rpdivcl  8363  rpgecl  8366  ge0p1rp  8369  elrpd  8375  ge0addcl  8600  ge0mulcl  8601  icoshftf1o  8609  peano2fzr  8651  uzsubsubfz  8661  fzsplit2  8664  elfznn  8668  fzss1  8676  fzss2  8677  fzp1elp1  8687  elfz1b  8702  elfz0fzfz0  8733  fz0fzelfz0  8734  difelfznle  8743  elfzofz  8768  fzosplitsnm1  8815  ubmelm1fzo  8832  fzofzp1b  8834  fzosplitsn  8839  frec2uzf1od  8853  frec2uzisod  8854  frecuzrdgrrn  8855  frec2uzrdg  8856  frecuzrdgrom  8857  frecuzrdgfn  8859  frecuzrdgsuc  8862  iseqfveq2  8885  expival  8891  expcl2lemap  8901  expclzaplem  8913  expge0  8925  expge1  8926  zsqcl2  8964  nn0abscl  9209  bj-inf2vnlem1  9400
  Copyright terms: Public domain W3C validator