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

Theorem syl6bi 254
 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 230 . 2 (𝜑 → (𝜓𝜒))
3 syl6bi.2 . 2 (𝜒𝜃)
42, 3syl6 35 1 (𝜑 → (𝜓𝜃))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 207 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 208 This theorem is referenced by:  ax12i  1962  sb3OLD  2503  sb1OLD  2505  sb4a  2507  hbsb2  2519  dfsb2  2530  2eu2  2737  nfabdw  3005  reu6  3721  2reu2  3886  sseq0  4357  disjel  4409  disjpss  4413  preq12b  4780  prneimg  4784  preqsnd  4788  elinti  4883  zfrepclf  5195  dtru  5268  opth1g  5367  sbcop1  5376  snopeqop  5393  propeqop  5394  otsndisj  5406  otiunsndisj  5407  iunopeqop  5408  po2ne  5488  soasym  5503  elreldm  5804  dfres3  5857  relcnvtrg  6117  relresfld  6125  ordtr2  6233  ordssun  6288  funopg  6386  funimass2  6434  f0dom0  6560  elfv2ex  6708  fveqdmss  6842  eldmrexrnb  6854  fvcofneq  6855  funopsn  6906  funopdmsn  6908  funsndifnop  6909  elunirn  7004  2f1fvneq  7012  oprabidw  7179  oprabid  7180  brfvopab  7203  limuni3  7555  peano5  7593  op1steq  7724  el2mpocsbcl  7771  bropopvvv  7776  bropfvvvv  7778  f1o2ndf1  7809  frxp  7811  fnwelem  7816  suppimacnv  7832  fvn0elsuppb  7838  suppfnss  7846  reldmtpos  7891  rntpos  7896  seqomlem2  8078  oaordi  8162  oa00  8175  oalimcl  8176  omeulem1  8198  nnaordi  8234  ecopovtrn  8390  undifixp  8487  mapdom2  8677  unxpdomlem3  8713  enp1i  8742  findcard2  8747  infssuni  8804  wdompwdom  9031  preleqg  9067  opthreg  9070  inf3lemd  9079  inf3lem2  9081  inf3lem6  9085  cnfcomlem  9151  cnfcom3  9156  karden  9313  carden2a  9384  alephdom  9496  dfac5lem4  9541  dfac12r  9561  kmlem2  9566  kmlem12  9576  cfslb2n  9679  alephsing  9687  fin23lem30  9753  fin1a2lem6  9816  fin1a2lem13  9823  axcc2lem  9847  domtriomlem  9853  axdc3lem2  9862  axdc4lem  9866  brdom6disj  9943  alephexp1  9990  pwfseq  10075  addnidpi  10312  indpi  10318  nqereu  10340  ltsonq  10380  distrlem5pr  10438  addcanpr  10457  suplem1pr  10463  suplem2pr  10464  ltsrpr  10488  ltsosr  10505  sqgt0sr  10517  leltne  10719  ltnsym  10727  ltlen  10730  eqlei  10739  eqlei2  10740  infm3  11589  nnunb  11882  0mnnnnn0  11918  elnnnn0b  11930  nn0ge2m1nn  11953  nn0le2is012  12035  btwnz  12073  uz11  12256  zqOLD  12344  xrleltne  12528  xltnegi  12599  xnn0lenn0nn0  12628  xnn0xadd0  12630  xmulasslem2  12665  reltxrnmnf  12725  icogelb  12778  iccleub  12782  uznfz  12980  2ffzeq  13018  elfzonlteqm1  13103  elfzo0l  13117  elfznelfzob  13133  elfzr  13140  elfzlmr  13141  injresinjlem  13147  injresinj  13148  fleqceilz  13212  modadd1  13266  modmul1  13282  modirr  13300  addmodlteq  13304  uzrdgfni  13316  fsuppmapnn0fiub0  13351  fsuppmapnn0ub  13353  seqf1o  13401  expnngt1  13592  hashrabsn01  13724  hashrabsn1  13725  hash1snb  13770  hash1n0  13772  hashf1lem2  13804  hash2prde  13818  hash2prd  13823  hash2pwpr  13824  hashle2pr  13825  hashle2prv  13826  hashge2el2dif  13828  hashge2el2difr  13829  fundmge2nop0  13840  ffz0iswrd  13881  ffz0iswrdOLD  13882  ccatrcl1  13938  pfxsuff1eqwrdeq  14051  wrdind  14074  wrd2ind  14075  swrdccatin1  14077  swrdccat3blem  14091  2cshwcshw  14177  cshwcsh2id  14180  cshimadifsn  14181  2swrd2eqwrdeq  14305  wwlktovf  14310  wwlktovfo  14312  s3sndisj  14317  s3iunsndisj  14318  relexpindlem  14412  rexico  14703  lo1le  14998  fsum2dlem  15115  ntrivcvg  15243  fprodss  15292  fprod2dlem  15324  0dvds  15620  mod2eq1n2dvds  15686  opoe  15702  omoe  15703  opeo  15704  omeo  15705  m1exp1  15717  nn0enne  15718  nn0o1gt2  15722  gcdneg  15860  dfgcd2  15884  algcvga  15913  eucalglt  15919  lcmf  15967  coprmdvds  15987  divgcdcoprmex  16000  cncongr1  16001  prm2orodd  16025  prm23lt5  16141  pockthi  16233  prmreclem5  16246  ramtcl2  16337  cshwrepswhash1  16426  f1ocpbl  16788  f1ovscpbl  16789  f1olecpbl  16790  monhom  16995  epihom  17002  inveq  17034  invcoisoid  17052  isocoinvid  17053  ciclcl  17062  cicrcl  17063  isinitoi  17253  istermoi  17254  2initoinv  17260  2termoinv  17267  setciso  17341  embedsetcestrclem  17397  ipopos  17760  gsumval2a  17884  ismnddef  17902  dfgrp2e  18059  symg2bas  18446  symgfix2  18464  gsmsymgreq  18480  pmtrdifellem4  18527  mndodcongi  18591  pj1eu  18742  cycsubmcmn  18928  dprd2da  19084  rimf1o  19406  rimrhm  19407  brric2  19420  lmodfopnelem1  19590  lspdisjb  19818  lspsnsubn0  19832  0ring01eq  19963  psrbaglefi  20071  obs2ss  20792  mamufacex  20919  mat0dim0  20995  mat0dimid  20996  mat0dimscm  20997  dmatmat  21022  scmatmat  21037  mat1scmat  21067  1mavmul  21076  mavmulsolcl  21079  gsummatr01  21187  cpmatpmat  21237  cpmadugsumlemF  21403  tg2  21492  tgcl  21496  neii1  21633  neii2  21635  neindisj2  21650  perfopn  21712  ordtbas2  21718  pnfnei  21747  mnfnei  21748  llyidm  22015  txlm  22175  qtopuni  22229  tgqtop  22239  isfild  22385  snfil  22391  fbunfip  22396  fgss2  22401  fmco  22488  fbflim2  22504  cnpflf2  22527  fcfelbas  22563  fcfneii  22564  alexsubALTlem2  22575  alexsubALT  22578  tgpconncompeqg  22638  tsmscl  22661  tngngpim  23186  tgioo  23322  xrsmopn  23338  iccntr  23347  reconnlem2  23353  addcnlem  23390  htpycn  23495  phtpyhtpy  23504  pi1blem  23561  fgcfil  23792  ioombl1lem4  24080  dyadmbl  24119  itg2gt0  24279  ditgneg  24373  dvivthlem1  24523  coeeq2  24750  aannenlem2  24836  sineq0  25027  efif1o  25046  leibpilem1OLD  25435  xrlimcnp  25463  vmacl  25612  efvmacl  25614  vmalelog  25698  dchrelbasd  25732  lgsqr  25844  lgsqrmodndvds  25846  gausslemma2dlem0i  25857  2lgslem2  25888  2lgs  25900  2lgsoddprmlem3  25907  2sqnn  25932  2sqreultlem  25940  2sqreultblem  25941  2sqreunnltlem  25943  2sqreunnltblem  25944  elntg2  26688  uhgr0vb  26774  umgrupgr  26805  umgrnloopv  26808  umgredgprv  26809  umgrislfupgrlem  26824  umgredg  26840  uspgrushgr  26877  uspgrupgr  26878  usgruspgr  26880  usgredgprvALT  26894  usgrnloopvALT  26900  uhgr2edg  26907  edg0usgr  26952  egrsubgr  26976  0uhgrsubgr  26978  uhgrspansubgrlem  26989  nbuhgr  27042  cusgrsize2inds  27152  cusgrfilem2  27155  vtxdg0v  27172  1loopgrnb0  27201  vtxdginducedm1lem4  27241  wlkvtxeledg  27322  wlkeq  27332  wlkl1loop  27336  wlk1walk  27337  upgrwlkedg  27340  uspgr2wlkeq  27344  wlkv0  27349  wlkonl1iedg  27364  wlkon2n0  27365  wlkp1lem8  27379  wlkp1  27380  lfgrwlkprop  27386  lfgrwlknloop  27388  2pthnloop  27429  upgrwlkdvde  27435  spthonepeq  27450  uhgrwkspthlem2  27452  usgr2wlkneq  27454  usgr2trlncl  27458  usgr2trlspth  27459  pthdlem2lem  27465  clwlkcompbp  27480  uspgrn2crct  27503  wwlks  27530  wwlknbp  27537  0enwwlksnge1  27559  wwlkswwlksn  27560  wlklnwwlkln1  27563  wwlksnextproplem3  27607  wwlksnextprop  27608  wspthsnonn0vne  27613  wspn0  27620  2pthon3v  27639  umgr2adedgspth  27644  rusgr0edg  27669  clwwlkccat  27685  clwlkclwwlklem2fv2  27691  clwlkclwwlklem2a4  27692  clwlkclwwlklem2  27695  clwlkclwwlkflem  27699  clwwlknp  27732  clwwlkwwlksb  27750  clwwlkext2edg  27752  erclwwlkneqlen  27764  hashecclwwlkn1  27773  umgrhashecclwwlk  27774  clwwlknonwwlknonb  27802  upgr1wlkdlem1  27841  upgr3v3e3cycl  27876  uhgr3cyclexlem  27877  1conngr  27890  conngrv2edg  27891  eupth2lem3lem4  27927  eulercrct  27938  isfrgr  27956  frgr3vlem2  27970  1to2vfriswmgr  27975  1to3vfriswmgr  27976  frgrncvvdeqlem9  28003  frgrwopreg  28019  frgr2wwlkeqm  28027  2wspmdisj  28033  numclwwlk1lem2f  28051  frgrreggt1  28089  frgrregord013  28091  frgrregord13  28092  l2p  28173  nmlno0lem  28487  normgt0  28821  ocin  28990  nmlnop0iALT  29689  nmopun  29708  cvpss  29979  cvnbtwn  29980  atcvati  30080  mdsymlem6  30102  iunrnmptss  30235  wrdt2ind  30544  issgon  31271  mbfmcnt  31415  ballotlemfc0  31639  ballotlemfcc  31640  satfv0  32492  satfv0fun  32505  fmla1  32521  gonarlem  32528  gonar  32529  goalrlem  32530  goalr  32531  fmla0disjsuc  32532  satffunlem  32535  satffunlem1lem1  32536  satffunlem2lem1  32538  satfun  32545  satfv0fvfmla0  32547  sategoelfv  32554  mthmblem  32714  sltintdifex  33055  sltres  33056  nosepnelem  33071  nolt02o  33086  pprodss4v  33232  funpartfun  33291  funpartfv  33293  5segofs  33354  btwnxfr  33404  brofs2  33425  brifs2  33426  btwnconn1  33449  segleantisym  33463  broutsideof2  33470  outsidene1  33471  outsidene2  33472  funray  33488  lineunray  33495  cldbnd  33561  bj-dtru  34026  bj-imdirval3  34356  topdifinffinlem  34500  isbasisrelowllem1  34508  isbasisrelowllem2  34509  relowlpssretop  34517  inunissunidif  34528  pibt2  34570  matunitlindf  34760  poimir  34795  volsupnfl  34807  itg2addnclem  34813  cover2  34860  sdclem2  34888  fdc  34891  sstotbnd3  34925  heibor1  34959  clmgmOLD  35000  smgrpmgm  35013  smgrpassOLD  35014  dvrunz  35103  0rngo  35176  lsatcvat  36056  lshpkrex  36124  cmtbr3N  36260  atn0  36314  atnle  36323  cvlsupr4  36351  cvlsupr5  36352  cvlsupr6  36353  cvrval4N  36420  cvratlem  36427  2llnjN  36573  2lplnj  36626  linepsubN  36758  elpaddatiN  36811  elpcliN  36899  pclcmpatN  36907  ldilval  37119  ltrnu  37127  cdleme18d  37301  tendotp  37767  tendof  37769  tendovalco  37771  diatrl  38050  diaintclN  38064  dvheveccl  38118  dibintclN  38173  dihord6apre  38262  dihmeetlem1N  38296  dihpN  38342  dihintcl  38350  dochkrshp4  38395  oexpreposd  39047  pw2f1ocnv  39502  iocinico  39686  infordmin  39767  pr2cv  39775  expgrowthi  40533  iotavalsb  40633  bi23imp1  40697  ioogtlb  41638  iocgtlb  41645  iocleub  41646  icoltub  41652  iooltub  41654  stoweidlem31  42185  oppr  43134  funressnfv  43147  eu2ndop1stv  43193  afvelrnb0  43232  otiunsndisjX  43347  el1fzopredsuc  43394  fzoopth  43396  2ffzoeq  43397  iccpartimp  43412  iccpartrn  43425  iccpartf  43426  iccpartnel  43433  fargshiftf  43435  fargshiftfo  43437  ichnfim  43459  ichreuopeq  43470  sprel  43481  sprsymrelfvlem  43487  sprsymrelfolem2  43490  prproropf1olem4  43503  prprelb  43513  poprelb  43521  fmtnofac1  43567  prmdvdsfmtnof1lem2  43582  31prm  43595  lighneallem3  43607  nn0o1gt2ALTV  43694  nn0oALTV  43696  odd2prm2  43718  mogoldbblem  43720  fpprbasnn  43729  fpprnn  43730  sbgoldbaltlem1  43779  nnsum3primesle9  43794  bgoldbtbndlem1  43805  bgoldbtbndlem2  43806  isomuspgrlem2d  43831  upwlkbprop  43848  mgmpropd  43877  clcllaw  43933  intop  43945  assintop  43951  assintopcllaw  43954  rngimf1o  44011  rngimrnghm  44012  c0snmgmhm  44020  elrngchom  44074  rnghmsubcsetclem1  44081  rnghmsubcsetclem2  44082  rngcid  44085  rngcinv  44087  rngciso  44088  elrngchomALTV  44092  rngccatidALTV  44095  rngcinvALTV  44099  rngcisoALTV  44100  funcrngcsetcALT  44105  zrinitorngc  44106  zrtermorngc  44107  elringchom  44120  rhmsubcsetclem1  44127  rhmsubcsetclem2  44128  ringcid  44131  rhmsubcrngclem1  44133  rhmsubcrngclem2  44134  ringcinv  44138  ringciso  44139  funcringcsetcALTV2lem7  44148  elringchomALTV  44155  ringccatidALTV  44158  ringcinvALTV  44162  ringcisoALTV  44163  funcringcsetclem7ALTV  44171  irinitoringc  44175  zrtermoringc  44176  rhmsubclem3  44194  rhmsubclem4  44195  rhmsubcALTVlem3  44212  rhmsubcALTVlem4  44213  ztprmneprm  44230  suppmptcfin  44262  linccl  44304  linc1  44315  lincolss  44324  ldepspr  44363  nn0sumshdiglem1  44516  rrxlines  44555  rrxsphere  44570  itsclc0yqsol  44586  itschlc0xyqsol1  44588
 Copyright terms: Public domain W3C validator