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  6416  nqnq0pi  6421  genipv  6492  addclpr  6520  nqprxx  6529  prmuloc  6547  mulclpr  6553  distrlem1prl  6558  distrlem1pru  6559  ltexprlempr  6582  ltexprlemrl  6584  ltexprlemru  6586  recexprlempr  6604  cauappcvgprlemm  6617  cauappcvgprlemopl  6618  cauappcvgprlemlol  6619  cauappcvgprlemopu  6620  cauappcvgprlemupu  6621  cauappcvgprlemloc  6624  cauappcvgprlemcl  6625  cauappcvgprlemladdfu  6626  cauappcvgprlemladdfl  6627  cauappcvgprlem2  6632  caucvgprlemm  6639  caucvgprlemopl  6640  caucvgprlemlol  6641  caucvgprlemopu  6642  caucvgprlemupu  6643  caucvgprlemloc  6646  caucvgprlemcl  6647  caucvgprlemladdfu  6648  caucvgprlem2  6651  receuap  7432  divvalap  7435  cju  7694  nn0ge2m1nn  8018  nnnegz  8024  elnnz  8031  elnn0z  8034  peano2z  8057  nn0n0n1ge2  8087  msqznn  8114  eluzaddi  8275  eluzsubi  8276  uzind4  8307  elnn1uz2  8320  uz2mulcl  8321  divfnzn  8332  nnrp  8367  rpaddcl  8381  rpmulcl  8382  rpdivcl  8383  rpgecl  8386  ge0p1rp  8389  elrpd  8395  ge0addcl  8620  ge0mulcl  8621  icoshftf1o  8629  peano2fzr  8671  uzsubsubfz  8681  fzsplit2  8684  elfznn  8688  fzss1  8696  fzss2  8697  fzp1elp1  8707  elfz1b  8722  elfz0fzfz0  8753  fz0fzelfz0  8754  difelfznle  8763  elfzofz  8788  fzosplitsnm1  8835  ubmelm1fzo  8852  fzofzp1b  8854  fzosplitsn  8859  frec2uzf1od  8873  frec2uzisod  8874  frecuzrdgrrn  8875  frec2uzrdg  8876  frecuzrdgrom  8877  frecuzrdgfn  8879  frecuzrdgsuc  8882  iseqfveq2  8905  expival  8911  expcl2lemap  8921  expclzaplem  8933  expge0  8945  expge1  8946  zsqcl2  8984  nn0abscl  9229  bj-nnord  9418  bj-inf2vnlem1  9430
  Copyright terms: Public domain W3C validator