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

Theorem syl6bi 243
Description: A mixed syllogism inference. (Contributed by NM, 2-Jan-1994.)
Hypotheses
Ref Expression
syl6bi.1 (𝜑 → (𝜓𝜒))
syl6bi.2 (𝜒𝜃)
Assertion
Ref Expression
syl6bi (𝜑 → (𝜓𝜃))

Proof of Theorem syl6bi
StepHypRef Expression
1 syl6bi.1 . . 3 (𝜑 → (𝜓𝜒))
21biimpd 219 . 2 (𝜑 → (𝜓𝜒))
3 syl6bi.2 . 2 (𝜒𝜃)
42, 3syl6 35 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
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 197
This theorem is referenced by:  ax12i  1877  sb3  2353  2eu2  2552  reu6  3389  sseq0  3966  disjel  4014  disjpss  4019  uneqdifeqOLD  4049  preq12b  4373  prel12  4374  prneimg  4379  elinti  4476  zfrepclf  4768  dtru  4848  opth1g  4937  propeqop  4960  otsndisj  4969  otiunsndisj  4970  iunopeqop  4971  elreldm  5339  issref  5497  relcnvtr  5643  relresfld  5650  ordtr2  5756  ordssun  5815  funopg  5910  funimass2  5960  f0dom0  6076  elfv2ex  6216  fveqdmss  6340  eldmrexrnb  6352  fvcofneq  6353  funopsn  6398  funopdmsn  6400  funsndifnop  6401  elunirn  6494  2f1fvneq  6502  oprabid  6662  brfvopab  6685  limuni3  7037  peano5  7074  op1steq  7195  el2mpt2csbcl  7235  bropopvvv  7240  bropfvvvv  7242  f1o2ndf1  7270  frxp  7272  fnwelem  7277  suppimacnv  7291  fvn0elsuppb  7297  suppfnss  7305  reldmtpos  7345  rntpos  7350  seqomlem2  7531  oaordi  7611  oa00  7624  oalimcl  7625  omeulem1  7647  nnaordi  7683  ecopovtrn  7835  undifixp  7929  mapdom2  8116  unxpdomlem3  8151  enp1i  8180  findcard2  8185  infssuni  8242  wdompwdom  8468  opthreg  8500  inf3lemd  8509  inf3lem2  8511  inf3lem6  8515  cnfcomlem  8581  cnfcom3  8586  karden  8743  carden2a  8777  alephdom  8889  dfac5lem4  8934  dfac12r  8953  kmlem2  8958  kmlem12  8968  cfslb2n  9075  alephsing  9083  fin23lem30  9149  fin1a2lem6  9212  fin1a2lem13  9219  axcc2lem  9243  domtriomlem  9249  axdc3lem2  9258  axdc4lem  9262  brdom6disj  9339  alephexp1  9386  pwfseq  9471  addnidpi  9708  indpi  9714  nqereu  9736  ltsonq  9776  distrlem5pr  9834  addcanpr  9853  suplem1pr  9859  suplem2pr  9860  ltsrpr  9883  ltsosr  9900  sqgt0sr  9912  leltne  10112  ltnsym  10120  ltlen  10123  eqlei  10132  eqlei2  10133  infm3  10967  nnunb  11273  0mnnnnn0  11310  elnnnn0b  11322  nn0ge2m1nn  11345  nn0le2is012  11426  btwnz  11464  uz11  11695  zq  11779  xrleltne  11963  xltnegi  12032  xnn0lenn0nn0  12060  xnn0xadd0  12062  xmulasslem2  12097  reltxrnmnf  12157  icogelb  12210  iccleub  12214  uznfz  12407  2ffzeq  12444  elfzonlteqm1  12527  elfzo0l  12542  elfznelfzob  12558  elfzr  12564  elfzlmr  12565  injresinjlem  12571  injresinj  12572  fleqceilz  12636  modadd1  12690  modmul1  12706  modirr  12724  addmodlteq  12728  uzrdgfni  12740  fsuppmapnn0fiub0  12776  fsuppmapnn0ub  12778  seqf1o  12825  hashrabsn01  13145  hashrabsn1  13146  hash1snb  13190  hash1n0  13192  hashf1lem2  13223  hash2prde  13235  hash2prd  13240  hash2pwpr  13241  hashle2pr  13242  hashle2prv  13243  hashge2el2dif  13245  hashge2el2difr  13246  fundmge2nop0  13257  ffz0iswrd  13315  ccatrcl1  13359  2swrd1eqwrdeq  13436  wrdind  13458  wrd2ind  13459  swrdccatin1  13464  swrdccat3blem  13476  2cshwcshw  13552  cshwcsh2id  13555  cshimadifsn  13556  2swrd2eqwrdeq  13677  wwlktovf  13680  wwlktovfo  13682  s3sndisj  13687  s3iunsndisj  13688  relexpindlem  13784  rexico  14074  lo1le  14363  fsum2dlem  14482  ntrivcvg  14610  fprodss  14659  fprod2dlem  14691  0dvds  14983  mod2eq1n2dvds  15052  opoe  15068  omoe  15069  opeo  15070  omeo  15071  m1exp1  15074  nn0enne  15075  nn0o1gt2  15078  gcdneg  15224  dfgcd2  15244  algcvga  15273  eucalglt  15279  lcmf  15327  coprmdvds  15347  divgcdcoprmex  15361  cncongr1  15362  prm2orodd  15385  prm23lt5  15500  pockthi  15592  prmreclem5  15605  ramtcl2  15696  cshwrepswhash1  15790  f1ocpbl  16166  f1ovscpbl  16167  f1olecpbl  16168  monhom  16376  epihom  16383  inveq  16415  invcoisoid  16433  isocoinvid  16434  ciclcl  16443  cicrcl  16444  isinitoi  16634  istermoi  16635  2initoinv  16641  2termoinv  16648  setciso  16722  embedsetcestrclem  16778  ipopos  17141  gsumval2a  17260  ismnddef  17277  dfgrp2e  17429  symg2bas  17799  symgfix2  17817  gsmsymgreq  17833  pmtrdifellem4  17880  mndodcongi  17943  pj1eu  18090  dprd2da  18422  rimf1o  18715  rimrhm  18716  brric2  18726  lmodfopnelem1  18880  lspdisjb  19107  lspsnsubn0  19121  0ring01eq  19252  psrbaglefi  19353  obs2ss  20054  mamufacex  20176  mat0dim0  20254  mat0dimid  20255  mat0dimscm  20256  dmatmat  20281  scmatmat  20296  mat1scmat  20326  1mavmul  20335  mavmulsolcl  20338  gsummatr01  20446  cpmatpmat  20496  cpmadugsumlemF  20662  tg2  20750  tgcl  20754  neii1  20891  neii2  20893  neindisj2  20908  perfopn  20970  ordtbas2  20976  pnfnei  21005  mnfnei  21006  llyidm  21272  txlm  21432  qtopuni  21486  tgqtop  21496  isfild  21643  snfil  21649  fbunfip  21654  fgss2  21659  fmco  21746  fbflim2  21762  cnpflf2  21785  fcfelbas  21821  fcfneii  21822  alexsubALTlem2  21833  alexsubALT  21836  tgpconncompeqg  21896  tsmscl  21919  tngngpim  22444  tgioo  22580  xrsmopn  22596  iccntr  22605  reconnlem2  22611  addcnlem  22648  htpycn  22753  phtpyhtpy  22762  pi1blem  22820  fgcfil  23050  ioombl1lem4  23310  dyadmbl  23349  itg2gt0  23508  ditgneg  23602  dvivthlem1  23752  coeeq2  23979  aannenlem2  24065  sineq0  24254  efif1o  24273  leibpilem1  24648  xrlimcnp  24676  vmacl  24825  efvmacl  24827  vmalelog  24911  dchrelbasd  24945  lgsqr  25057  gausslemma2dlem0i  25070  2lgslem2  25101  2lgs  25113  2lgsoddprmlem3  25120  uhgr0vb  25948  umgrupgr  25979  umgrnloopv  25982  umgredgprv  25983  umgrislfupgrlem  25998  umgredg  26014  uspgrushgr  26051  uspgrupgr  26052  usgruspgr  26054  usgredgprvALT  26068  usgrnloopvALT  26074  uhgr2edg  26081  edg0usgr  26126  egrsubgr  26150  0uhgrsubgr  26152  uhgrspansubgrlem  26163  nbuhgr  26220  nbgrisvtx  26236  uvtxaisvtx  26270  vtxnbuvtx  26272  uvtx2vtx1edg  26280  cusgrsize2inds  26330  cusgrfilem2  26333  vtxdg0v  26350  1loopgrnb0  26379  vtxdginducedm1lem4  26419  wlkvtxeledg  26500  wlkeq  26510  wlkl1loop  26515  wlk1walk  26516  upgrwlkedg  26519  uspgr2wlkeq  26523  wlkv0  26528  wlkonl1iedg  26542  wlkon2n0  26543  wlkp1lem8  26558  wlkp1  26559  lfgrwlkprop  26565  lfgrwlknloop  26567  upgrwlkdvde  26614  spthonepeq  26629  uhgrwkspthlem2  26631  usgr2wlkneq  26633  usgr2trlncl  26637  usgr2trlspth  26638  pthdlem2lem  26644  uspgrn2crct  26681  wwlks  26708  wwlknbp  26714  0enwwlksnge1  26730  wwlkswwlksn  26731  wlklnwwlkln1  26735  wwlksnextproplem3  26787  wwlksnextprop  26788  wspthsnonn0vne  26794  2pthon3v  26820  umgr2adedgspth  26825  wwlks2onv  26828  rusgr0edg  26849  clwwlknclwwlkdifs  26854  clwwlknbp0  26865  isclwwlksnx  26870  clwwlkclwwlkn  26872  clwlkclwwlklem2fv2  26878  clwlkclwwlklem2a4  26879  clwlkclwwlklem2  26882  clwwlksext2edg  26903  erclwwlksneqlen  26925  hashecclwwlksn1  26934  umgrhashecclwwlk  26935  clwlksfclwwlk  26942  clwlksf1clwwlklem  26948  upgr1wlkdlem1  26985  upgr3v3e3cycl  27020  uhgr3cyclexlem  27021  1conngr  27034  conngrv2edg  27035  eupth2lem3lem4  27071  eulercrct  27082  frgrusgrfrcond  27103  frgr3vlem2  27118  1to2vfriswmgr  27123  1to3vfriswmgr  27124  frgrncvvdeqlem9  27151  frgrwopreg  27159  frgr2wwlkeqm  27169  2wspmdisj  27175  numclwwlkovf2ex  27191  numclwlk1lem2f1  27198  frgrreggt1  27221  frgrregord013  27223  frgrregord13  27224  l2p  27301  nmlno0lem  27618  normgt0  27954  ocin  28125  nmlnop0iALT  28824  nmopun  28843  cvpss  29114  cvnbtwn  29115  atcvati  29215  mdsymlem6  29237  issgon  30160  mbfmcnt  30304  ballotlemfc0  30528  ballotlemfcc  30529  mthmblem  31451  dfres3  31624  soasym  31633  sltintdifex  31788  sltres  31789  nosepnelem  31804  nolt02o  31819  pprodss4v  31966  funpartfun  32025  funpartfv  32027  5segofs  32088  btwnxfr  32138  brofs2  32159  brifs2  32160  btwnconn1  32183  segleantisym  32197  broutsideof2  32204  outsidene1  32205  outsidene2  32206  funray  32222  lineunray  32229  cldbnd  32296  bj-dtru  32772  bj-ismoored0  33036  topdifinffinlem  33166  isbasisrelowllem1  33174  isbasisrelowllem2  33175  relowlpssretop  33183  matunitlindf  33378  poimir  33413  volsupnfl  33425  itg2addnclem  33432  cover2  33479  sdclem2  33509  fdc  33512  sstotbnd3  33546  heibor1  33580  clmgmOLD  33621  smgrpmgm  33634  smgrpassOLD  33635  dvrunz  33724  0rngo  33797  lsatcvat  34156  lshpkrex  34224  cmtbr3N  34360  atn0  34414  atnle  34423  cvlsupr4  34451  cvlsupr5  34452  cvlsupr6  34453  cvrval4N  34519  cvratlem  34526  2llnjN  34672  2lplnj  34725  linepsubN  34857  elpaddatiN  34910  elpcliN  34998  pclcmpatN  35006  ldilval  35218  ltrnu  35226  cdleme18d  35401  tendotp  35868  tendof  35870  tendovalco  35872  diatrl  36152  diaintclN  36166  dvheveccl  36220  dibintclN  36275  dihord6apre  36364  dihmeetlem1N  36398  dihpN  36444  dihintcl  36452  dochkrshp4  36497  pw2f1ocnv  37423  iocinico  37616  expgrowthi  38352  iotavalsb  38454  bi23imp1  38521  ioogtlb  39520  iocgtlb  39527  iocleub  39528  icoltub  39535  iooltub  39538  stoweidlem31  40011  2reu2  40950  eu2ndop1stv  40965  funressnfv  40971  afvelrnb0  41007  otiunsndisjX  41061  el1fzopredsuc  41098  fzoopth  41100  2ffzoeq  41101  iccpartimp  41117  iccpartrn  41130  iccpartf  41131  iccpartnel  41138  fargshiftf  41140  fargshiftfo  41142  pfxsuff1eqwrdeq  41172  fmtnofac1  41247  prmdvdsfmtnof1lem2  41262  31prm  41277  lighneallem3  41289  nn0o1gt2ALTV  41370  nn0oALTV  41372  odd2prm2  41392  mogoldbblem  41394  sbgoldbaltlem1  41432  nnsum3primesle9  41447  bgoldbtbndlem1  41458  bgoldbtbndlem2  41459  upwlkbprop  41484  sprel  41499  sprsymrelfvlem  41505  sprsymrelfolem2  41508  mgmpropd  41540  clcllaw  41592  intop  41604  assintop  41610  assintopcllaw  41613  rngimf1o  41670  rngimrnghm  41671  c0snmgmhm  41679  elrngchom  41733  rnghmsubcsetclem1  41740  rnghmsubcsetclem2  41741  rngcid  41744  rngcinv  41746  rngciso  41747  elrngchomALTV  41751  rngccatidALTV  41754  rngcinvALTV  41758  rngcisoALTV  41759  funcrngcsetcALT  41764  zrinitorngc  41765  zrtermorngc  41766  elringchom  41779  rhmsubcsetclem1  41786  rhmsubcsetclem2  41787  ringcid  41790  rhmsubcrngclem1  41792  rhmsubcrngclem2  41793  ringcinv  41797  ringciso  41798  funcringcsetcALTV2lem7  41807  elringchomALTV  41814  ringccatidALTV  41817  ringcinvALTV  41821  ringcisoALTV  41822  funcringcsetclem7ALTV  41830  irinitoringc  41834  zrtermoringc  41835  rhmsubclem3  41853  rhmsubclem4  41854  rhmsubcALTVlem3  41871  rhmsubcALTVlem4  41872  ztprmneprm  41890  suppmptcfin  41925  linccl  41968  linc1  41979  lincolss  41988  ldepspr  42027  nn0sumshdiglem1  42180
  Copyright terms: Public domain W3C validator