MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl5ibcom Structured version   Visualization version   GIF version

Theorem syl5ibcom 233
Description: A mixed syllogism inference. (Contributed by NM, 19-Jun-2007.)
Hypotheses
Ref Expression
syl5ib.1 (𝜑𝜓)
syl5ib.2 (𝜒 → (𝜓𝜃))
Assertion
Ref Expression
syl5ibcom (𝜑 → (𝜒𝜃))

Proof of Theorem syl5ibcom
StepHypRef Expression
1 syl5ib.1 . . 3 (𝜑𝜓)
2 syl5ib.2 . . 3 (𝜒 → (𝜓𝜃))
31, 2syl5ib 232 . 2 (𝜒 → (𝜑𝜃))
43com12 32 1 (𝜑 → (𝜒𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 195
This theorem is referenced by:  biimpcd  237  elrab3t  3326  mob2  3349  rmob  3491  sneqrg  4302  preq1b  4309  disjxun  4572  sotric  4972  sotrieq  4973  iss  5351  poirr2  5423  xp11  5471  nordeq  5642  nsuceq0  5705  suctrOLD  5709  ordequn  5728  tz6.12c  6105  fnbrfvb  6128  foeqcnvco  6430  f1eqcocnv  6431  dfwe2  6847  mpt2sn  7129  tfrlem15  7349  tz7.44-2  7364  tz7.48-1  7399  tz7.49  7401  oawordexr  7497  oewordi  7532  oeeulem  7542  nna0r  7550  nnawordex  7578  nnaordex  7579  oaabs  7585  oaabs2  7586  ectocld  7675  ecoptocl  7698  mapsn  7759  eqeng  7849  difsnen  7901  fopwdom  7927  frfi  8064  elfiun  8193  ordiso  8278  ordtypelem7  8286  wemaplem2  8309  suc11reg  8373  inf3lem6  8387  noinfep  8414  cantnff  8428  cantnfp1lem2  8433  cantnfp1lem3  8434  cantnflem1  8443  cantnf  8447  r111  8495  rankc2  8591  tcrank  8604  cardnueq0  8647  fodomfi2  8740  alephinit  8775  dfac9  8815  dfac12k  8826  cdainf  8871  ackbij1  8917  ackbij2  8922  sornom  8956  fin23lem16  9014  fin23lem21  9018  isf32lem2  9033  fin1a2lem6  9084  itunitc  9100  zorn2lem4  9178  wunr1om  9394  tskr1om  9442  recmulnq  9639  ltexnq  9650  distrlem4pr  9701  1re  9892  0re  9893  0cnALT  10118  mulge0  10392  prodgt0  10714  peano2nn  10876  recnz  11281  zneo  11289  uzn0  11532  xlemul1a  11944  prunioo  12125  flidz  12425  ceilidz  12465  modid2  12511  modmuladdnn0  12528  om2uzrani  12565  uzrdgfni  12571  seqid  12660  seqz  12663  facdiv  12888  facwordi  12890  hashdom  12978  wrdnval  13133  wrdl1s1  13190  sqrmo  13783  fsumf1o  14244  isumltss  14362  supcvg  14370  dvdsnegb  14780  odd2np1lem  14845  odd2np1  14846  ltoddhalfle  14866  halfleoddlt  14867  opoe  14868  omoe  14869  opeo  14870  omeo  14871  bitsuz  14977  bezoutlem4  15040  gcddiv  15049  gcdzeq  15052  dvdssqim  15054  lcmgcdeq  15106  coprmdvds2  15149  rpmul  15154  divgcdcoprmex  15161  cncongr2  15163  dvdsprm  15196  coprm  15204  prmdvdsexp  15208  prmdiv  15271  pythagtriplem19  15319  pc2dvds  15364  pcadd  15374  prmpwdvds  15389  vdwlem11  15476  ramubcl  15503  0ram  15505  mreexexdOLD  16075  posasymb  16718  pleval2  16731  pltval3  16733  plttr  16736  pospo  16739  letsr  16993  intopsn  17019  ismgmid  17030  imasmnd2  17093  isgrpid2  17224  isgrpinv  17238  dfgrp3lem  17279  imasgrp2  17296  orbsta  17512  symgfix2  17602  pmtrfrn  17644  pmtrrn2  17646  odmulg  17739  odmulgeq  17740  gexdvdsi  17764  gexnnod  17769  pgpssslw  17795  sylow2alem1  17798  fislw  17806  lsmss1b  17846  lsmss2b  17848  efgrelexlemb  17929  torsubg  18023  ablfacrplem  18230  pgpfac1lem2  18240  pgpfac1lem3  18242  imasring  18385  dvdsrcl2  18416  dvdsrtr  18418  dvdsrmul1  18419  irredn0  18469  lspsneq0  18776  lmhmima  18811  lspsolv  18907  opsrtoslem2  19249  mpfind  19300  mpfpf1  19479  pf1mpf  19480  xrsdsreclblem  19554  dvdsrzring  19593  prmirredlem  19602  znunit  19673  pjdm2  19813  obselocv  19830  lindfrn  19918  cpmadugsumlemF  20439  baspartn  20508  bastop  20535  iscld3  20617  isopn3  20619  iscldtop  20648  ordtrest2lem  20756  2ndcredom  21002  2ndc1stc  21003  2ndcrest  21006  2ndcdisj  21008  2ndcsep  21011  kgenidm  21099  dfac14  21170  tx2ndc  21203  kqreglem1  21293  rnelfm  21506  fmfnfmlem2  21508  fmfnfmlem4  21510  fmfnfm  21511  flimtopon  21523  fclstopon  21565  xrsmopn  22352  icccmplem2  22363  reconnlem1  22366  iccpnfcnv  22479  cphsqrtcl2  22715  ivthlem3  22943  ivthicc  22948  ovolctb  22979  ioombl  23054  itgabs  23321  itgsplitioo  23324  dvlip  23474  c1liplem1  23477  c1lip1  23478  dvgt0lem1  23483  dvivthlem2  23490  dvne0  23492  lhop1lem  23494  lhop1  23495  lhop2  23496  lhop  23497  dvcvx  23501  itgsubstlem  23529  mdegnn0cl  23549  ig1peu  23649  elply2  23670  plypf1  23686  dgreq0  23739  aannenlem3  23803  abelthlem2  23904  lognegb  24054  eflogeq  24066  efopn  24118  cxpge0  24143  cxplea  24156  cxple2  24157  cxpcn3lem  24202  cxpaddlelem  24206  cxpaddle  24207  cxpeq  24212  asinsinb  24338  acoscosb  24339  atantanb  24365  leibpilem1  24381  wilthlem2  24509  sqf11  24579  sqff1o  24622  ppiublem1  24641  lgsdir  24771  lgsne0  24774  lgsquadlem3  24821  2sqblem  24870  dchrisum0flblem1  24911  ostth3  25041  ostth  25042  colinearalg  25505  axcontlem5  25563  axcontlem9  25567  umgraf  25610  uslgraf1oedg  25651  nbgrassvwo  25729  usgrcyclnl1  25931  nvnencycllem  25934  clwwlknprop  26063  clwlkf1clwwlklem1  26136  usg2wlkonot  26173  usg2wotspth  26174  eupath2lem2  26268  eupath2lem3  26269  htthlem  26961  pjpreeq  27444  h1dn0  27598  spansneleqi  27615  rnbra  28153  dfpjop  28228  elpjrn  28236  stm1i  28289  mdbr2  28342  mdsl2i  28368  sumdmdlem  28464  dmdbr6ati  28469  ordtrest2NEWlem  29099  xrge0iifcnv  29110  eulerpartlemb  29560  erdszelem8  30237  cvmlift3lem4  30361  cvmlift3lem5  30362  mrsub0  30470  mrsubccat  30472  mrsubcn  30473  msubrn  30483  msrid  30499  elmthm  30530  dvdspw  30692  dfon2lem9  30743  poseq  30797  noseponlem  30868  nodenselem3  30885  nodenselem5  30887  nodenselem8  30890  nofulllem5  30908  btwnconn1lem11  31177  broutsideof2  31202  opnbnd  31293  tailfb  31345  fin2so  32366  poimirlem9  32388  poimirlem17  32396  poimirlem26  32405  poimirlem27  32406  poimirlem31  32410  itgabsnc  32449  ftc2nc  32464  sdclem2  32508  subspopn  32518  equivtotbnd  32547  rngosn3  32693  igenval2  32835  isfldidl  32837  lshpinN  33094  lsatcv0eq  33152  lsatcv1  33153  cvrnbtwn3  33381  cvrnbtwn4  33384  cvrcmp  33388  atnlt  33418  cvlexchb1  33435  2llnne2N  33512  atcvr0eq  33530  lnnat  33531  cvrat4  33547  ps-1  33581  3at  33594  llncmp  33626  llnnlt  33627  llncvrlpln2  33661  llncvrlpln  33662  lplncmp  33666  lplnnlt  33669  lplncvrlvol2  33719  lplncvrlvol  33720  lvolcmp  33721  lvolnltN  33722  dalempnes  33755  dalemqnet  33756  dalem-cly  33775  dalem44  33820  lncmp  33887  cdlemblem  33897  llnexch2N  33974  osumcllem4N  34063  pexmidlem1N  34074  lhp2atnle  34137  cdleme11dN  34367  cdleme20k  34425  cdleme21at  34434  cdleme21ct  34435  cdleme32e  34551  cdleme35f  34560  tendoex  35081  dochexmidlem1  35567  lcfrlem9  35657  mapd1o  35755  mapdindp3  35829  ismrc  36082  pellexlem1  36211  aomclem4  36445  dfac21  36454  lsmfgcl  36462  lmhmfgima  36472  dfacbasgrp  36497  hbtlem6  36518  fiuneneq  36594  mapsnd  38183  stoweidlem27  38721  stoweidlem29  38723  iccpartrn  39770  prmdvdsfmtnof1lem2  39837  mod42tp1mod8  39859  uhgrn0  40288  upgrfn  40312  umgrfn  40323  uspgrf1oedg  40402  uvtxanbgrvtx  40618  vtxduhgr0nedg  40706  pthdivtx  40934  iswwlksnx  41041  clwlksf1clwwlklem1  41271  eupth2lem2  41386  eupth2lem3lem6  41400  assintopass  41639
  Copyright terms: Public domain W3C validator