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

Theorem sylanbrc 413
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 304 . 2 (𝜑 → (𝜓𝜒))
4 sylanbrc.3 . 2 (𝜃 ↔ (𝜓𝜒))
53, 4sylibr 133 1 (𝜑𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  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:  sb2  1740  sbequ1  1741  sbidm  1823  eqeu  2854  euind  2871  reuind  2889  eldifd  3081  eqssd  3114  ssrabdv  3176  elind  3261  dcun  3473  opm  4159  issod  4244  ordsucim  4419  onintonm  4436  ordtri2or2exmidlem  4444  en2lp  4472  ordwe  4493  sosng  4615  sotri2  4939  sotri3  4940  relssdmrn  5062  funun  5170  fnsng  5173  fnprg  5181  fntpg  5182  fntp  5183  fununi  5194  imain  5208  fnco  5234  f00  5317  f1ss  5337  f1ssr  5338  f1ssres  5340  f1f1orn  5381  foimacnv  5388  foun  5389  fun11iun  5391  sefvex  5445  dff3im  5568  fmpt  5573  ffnfv  5581  fmpt2d  5585  ffvresb  5586  fprg  5606  foco2  5658  fcof1  5687  fcofo  5688  fcof1o  5693  fliftf  5703  isoini2  5723  f1oiso  5730  moriotass  5761  fnoprabg  5875  f1ocnvd  5975  suppssfv  5981  suppssov1  5982  1stcof  6064  2ndcof  6065  1stconst  6121  2ndconst  6122  fo2ndf  6127  f1o2ndf1  6128  f1od2  6135  smores2  6194  tfrlem5  6214  tfrlemibfn  6228  tfr1onlembfn  6244  tfri1dALT  6251  tfrcllembfn  6257  nntri2  6393  eroveu  6523  elixpsn  6632  dom2lem  6669  xpf1o  6741  fidifsnen  6767  finexdc  6799  unfidisj  6813  f1finf1o  6838  fidcenumlemrks  6844  sbthlemi9  6856  supeuti  6884  infeuti  6919  casef1  6978  caseinl  6979  caseinr  6980  difinfsnlem  6987  ctmlemr  6996  ctm  6997  ctssdclemn0  6998  ctssdccl  6999  ctssdc  7001  enumctlemm  7002  nnnninf  7026  en2other2  7064  exmidfodomrlemim  7069  cc2lem  7093  cc4f  7096  addclpi  7154  mulclpi  7155  nnppipi  7170  recmulnqg  7218  enq0ref  7260  nqnq0pi  7265  genipv  7336  addclpr  7364  nqprxx  7373  prmuloc  7393  mulclpr  7399  distrlem1prl  7409  distrlem1pru  7410  ltexprlempr  7435  ltexprlemrl  7437  ltexprlemru  7439  lteupri  7444  recexprlempr  7459  cauappcvgprlemm  7472  cauappcvgprlemopl  7473  cauappcvgprlemlol  7474  cauappcvgprlemopu  7475  cauappcvgprlemupu  7476  cauappcvgprlemloc  7479  cauappcvgprlemcl  7480  cauappcvgprlemladdfu  7481  cauappcvgprlemladdfl  7482  cauappcvgprlem2  7487  caucvgprlemm  7495  caucvgprlemopl  7496  caucvgprlemlol  7497  caucvgprlemopu  7498  caucvgprlemupu  7499  caucvgprlemloc  7502  caucvgprlemcl  7503  caucvgprlemladdfu  7504  caucvgprlem2  7507  caucvgprprlemml  7521  caucvgprprlemmu  7522  caucvgprprlemopl  7524  caucvgprprlemlol  7525  caucvgprprlemopu  7526  caucvgprprlemupu  7527  caucvgprprlemloc  7530  caucvgprprlemcl  7531  caucvgprprlem2  7537  suplocexprlemex  7549  suplocsrlem  7635  elrealeu  7656  rereceu  7716  axpre-suploclemres  7728  negf1o  8163  receuap  8449  divvalap  8453  cju  8738  nn0ge2m1nn  9056  nnnegz  9076  elnnz  9083  elnn0z  9086  peano2z  9109  nn0n0n1ge2  9140  msqznn  9170  eluzaddi  9371  eluzsubi  9372  uzind4  9405  supinfneg  9412  infsupneg  9413  elnn1uz2  9423  uz2mulcl  9424  divfnzn  9435  nnrp  9473  rpaddcl  9487  rpmulcl  9488  rpdivcl  9489  rpgecl  9492  ge0p1rp  9495  elrpd  9503  ge0addcl  9787  ge0mulcl  9788  ge0xaddcl  9789  icoshftf1o  9797  peano2fzr  9841  uzsubsubfz  9851  fzsplit2  9854  elfznn  9858  fzss1  9867  fzss2  9868  fzp1elp1  9879  elfz1b  9894  elfz0fzfz0  9927  fz0fzelfz0  9928  difelfznle  9936  elfzofz  9963  fzosplitsnm1  10010  ubmelm1fzo  10027  fzofzp1b  10029  fzosplitsn  10034  exbtwnz  10052  flqge0nn0  10090  flqge1nn  10091  zmodcl  10141  modqmuladdnn0  10165  modsumfzodifsn  10193  frec2uzf1od  10203  frec2uzisod  10204  frecuzrdgrrn  10205  frec2uzrdg  10206  frecuzrdgrcl  10207  frecuzrdgtcl  10209  frecuzrdgsuc  10211  frecuzrdgrclt  10212  frecuzrdgfunlem  10216  frecuzrdgtclt  10218  frecuzrdgsuctlem  10220  uzennn  10233  seq3fveq2  10266  monoord  10273  iseqf1olemqcl  10283  iseqf1olemnab  10285  iseqf1olemab  10286  iseqf1olemqf1o  10290  seq3f1olemqsumkj  10295  seq3f1olemqsumk  10296  seq3id2  10306  exp3val  10319  expcl2lemap  10329  expclzaplem  10341  expge0  10353  expge1  10354  zsqcl2  10394  bcval4  10522  bcn1  10528  bccl2  10538  hashennnuni  10549  hashunlem  10574  hashdifpr  10590  zfz1isolem1  10607  seq3coll  10609  shftfn  10620  shftf  10626  recvguniq  10791  resqrexlemdecn  10808  rersqreu  10824  nn0abscl  10881  nnabscl  10896  abs2dif  10902  climuni  11086  2clim  11094  climcn2  11102  summodclem2a  11174  fsum3  11180  fsum3cvg3  11189  fsumcl2lem  11191  fsumadd  11199  fisum0diag2  11240  fsummulc2  11241  fsumge0  11252  geolim2  11305  cvgratnnlemabsle  11320  cvgratz  11325  mertenslemi1  11328  prodmodclem3  11368  prodmodclem2a  11369  eff2  11410  tanvalap  11438  zdvdsdc  11537  fzo0dvdseq  11578  oexpneg  11597  oddge22np1  11601  evennn02n  11602  evennn2n  11603  nno  11626  divalglemeunn  11641  divalglemex  11642  divalglemeuneg  11643  divalg  11644  zsupcllemstep  11661  zsupcl  11663  divgcdz  11683  bezoutlemmain  11709  bezoutlemmo  11717  bezoutlemeu  11718  bezoutlemle  11719  sqgcd  11740  eucalgval2  11757  eucalglt  11761  lcmcllem  11771  lcmledvds  11774  lcmneg  11778  lcmgcdlem  11781  ncoprmgcdne1b  11793  prmind2  11824  sqnprm  11839  isprm6  11848  sqrt2irrlem  11862  pw2dvdseu  11869  sqpweven  11876  2sqpwodd  11877  sqrt2irrap  11881  qgt0numnn  11900  phicl2  11913  hashdvds  11920  crth  11923  phimullem  11924  hashgcdlem  11926  oddennn  11928  evenennn  11929  ennnfoneleminc  11947  ennnfonelemf1  11954  ennnfonelemen  11957  exmidunben  11962  ctinf  11966  ctiunctlemfo  11975  tgtopon  12261  distopon  12282  epttop  12285  resttopon  12366  resttopon2  12373  cnco  12416  lmss  12441  txtopon  12457  uptx  12469  txdis1cn  12473  hmeocnv  12502  hmeof1o2  12503  hmeores  12510  hmeoco  12511  idhmeo  12512  txhmeo  12514  txswaphmeo  12516  psmetxrge0  12527  isxmet2d  12543  metres2  12576  xmetresbl  12635  comet  12694  bdxmet  12696  bdmet  12697  tgioo  12741  mulc1cncf  12771  mulcncflem  12785  cnrehmeocntop  12788  cnopnap  12789  dedekindeu  12796  dedekindicclemicc  12805  ivthinclemlm  12807  ivthinclemum  12808  ivthinclemlopn  12809  ivthinclemlr  12810  ivthinclemuopn  12811  ivthinclemur  12812  ivthinclemloc  12814  ivthinc  12816  dvfgg  12852  dvcjbr  12867  dvcj  12868  dvfre  12869  rplogbval  13055  bj-nnord  13300  bj-inf2vnlem1  13312  pwf1oexmid  13340  nnsf  13347  nninfall  13352  nninfself  13357  exmidsbthrlem  13365  qdencn  13370
  Copyright terms: Public domain W3C validator