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

Theorem syl6bi 244
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 220 . 2 (𝜑 → (𝜓𝜒))
3 syl6bi.2 . 2 (𝜒𝜃)
42, 3syl6 35 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197
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 198
This theorem is referenced by:  ax12i  2060  sb3  2515  2eu2  2729  reu6  3604  sseq0  4184  disjel  4232  disjpss  4236  preq12b  4580  prel12OLD  4581  prneimg  4586  preqsnd  4590  elinti  4689  zfrepclf  4984  dtru  5053  opth1g  5149  snopeqop  5173  propeqop  5175  otsndisj  5187  otiunsndisj  5188  iunopeqop  5189  elreldm  5565  dfres3  5616  idrefOLD  5734  relcnvtr  5883  relresfld  5890  ordtr2  5994  ordssun  6050  funopg  6145  funimass2  6193  f0dom0  6314  elfv2ex  6459  fveqdmss  6586  eldmrexrnb  6598  fvcofneq  6599  funopsn  6647  funopdmsn  6649  funsndifnop  6650  elunirn  6743  2f1fvneq  6751  oprabid  6915  brfvopab  6940  limuni3  7292  peano5  7329  op1steq  7452  el2mpt2csbcl  7493  bropopvvv  7499  bropfvvvv  7501  f1o2ndf1  7529  frxp  7531  fnwelem  7536  suppimacnv  7550  fvn0elsuppb  7556  suppfnss  7564  suppfnssOLD  7565  reldmtpos  7605  rntpos  7610  seqomlem2  7792  oaordi  7873  oa00  7886  oalimcl  7887  omeulem1  7909  nnaordi  7945  ecopovtrn  8096  undifixp  8191  mapdom2  8380  unxpdomlem3  8415  enp1i  8444  findcard2  8449  infssuni  8506  wdompwdom  8732  preleqg  8767  opthreg  8770  opthregOLD  8772  inf3lemd  8781  inf3lem2  8783  inf3lem6  8787  cnfcomlem  8853  cnfcom3  8858  karden  9015  carden2a  9085  alephdom  9197  dfac5lem4  9242  dfac12r  9263  kmlem2  9268  kmlem12  9278  cfslb2n  9385  alephsing  9393  fin23lem30  9459  fin1a2lem6  9522  fin1a2lem13  9529  axcc2lem  9553  domtriomlem  9559  axdc3lem2  9568  axdc4lem  9572  brdom6disj  9649  alephexp1  9696  pwfseq  9781  addnidpi  10018  indpi  10024  nqereu  10046  ltsonq  10086  distrlem5pr  10144  addcanpr  10163  suplem1pr  10169  suplem2pr  10170  ltsrpr  10193  ltsosr  10210  sqgt0sr  10222  leltne  10422  ltnsym  10430  ltlen  10433  eqlei  10442  eqlei2  10443  infm3  11277  nnunb  11575  0mnnnnn0  11611  elnnnn0b  11623  nn0ge2m1nn  11646  nn0le2is012  11727  btwnz  11765  uz11  11947  zq  12033  xrleltne  12214  xltnegi  12285  xnn0lenn0nn0  12313  xnn0xadd0  12315  xmulasslem2  12350  reltxrnmnf  12410  icogelb  12463  iccleub  12467  uznfz  12666  2ffzeq  12704  elfzonlteqm1  12788  elfzo0l  12802  elfznelfzob  12818  elfzr  12825  elfzlmr  12826  injresinjlem  12832  injresinj  12833  fleqceilz  12897  modadd1  12951  modmul1  12967  modirr  12985  addmodlteq  12989  uzrdgfni  13001  fsuppmapnn0fiub0  13036  fsuppmapnn0ub  13038  seqf1o  13085  hashrabsn01  13400  hashrabsn1  13401  hash1snb  13444  hash1n0  13446  hashf1lem2  13477  hash2prde  13489  hash2prd  13494  hash2pwpr  13495  hashle2pr  13496  hashle2prv  13497  hashge2el2dif  13499  hashge2el2difr  13500  fundmge2nop0  13511  ffz0iswrd  13563  ccatrcl1  13611  2swrd1eqwrdeq  13698  wrdind  13720  wrd2ind  13721  swrdccatin1  13727  swrdccat3blem  13739  2cshwcshw  13815  cshwcsh2id  13818  cshimadifsn  13819  2swrd2eqwrdeq  13941  wwlktovf  13944  wwlktovfo  13946  s3sndisj  13951  s3iunsndisj  13952  relexpindlem  14046  rexico  14336  lo1le  14625  fsum2dlem  14744  ntrivcvg  14870  fprodss  14919  fprod2dlem  14951  0dvds  15245  mod2eq1n2dvds  15311  opoe  15327  omoe  15328  opeo  15329  omeo  15330  m1exp1  15333  nn0enne  15334  nn0o1gt2  15337  gcdneg  15482  dfgcd2  15502  algcvga  15531  eucalglt  15537  lcmf  15585  coprmdvds  15605  divgcdcoprmex  15618  cncongr1  15619  prm2orodd  15642  prm23lt5  15756  pockthi  15848  prmreclem5  15861  ramtcl2  15952  cshwrepswhash1  16041  f1ocpbl  16410  f1ovscpbl  16411  f1olecpbl  16412  monhom  16619  epihom  16626  inveq  16658  invcoisoid  16676  isocoinvid  16677  ciclcl  16686  cicrcl  16687  isinitoi  16877  istermoi  16878  2initoinv  16884  2termoinv  16891  setciso  16965  embedsetcestrclem  17022  ipopos  17385  gsumval2a  17504  ismnddef  17521  dfgrp2e  17673  symg2bas  18039  symgfix2  18057  gsmsymgreq  18073  pmtrdifellem4  18120  mndodcongi  18183  pj1eu  18330  dprd2da  18663  rimf1o  18958  rimrhm  18959  brric2  18969  lmodfopnelem1  19123  lspdisjb  19353  lspsnsubn0  19368  0ring01eq  19500  psrbaglefi  19601  obs2ss  20304  mamufacex  20426  mat0dim0  20505  mat0dimid  20506  mat0dimscm  20507  dmatmat  20532  scmatmat  20547  mat1scmat  20577  1mavmul  20586  mavmulsolcl  20589  gsummatr01  20698  cpmatpmat  20749  cpmadugsumlemF  20915  tg2  21004  tgcl  21008  neii1  21145  neii2  21147  neindisj2  21162  perfopn  21224  ordtbas2  21230  pnfnei  21259  mnfnei  21260  llyidm  21526  txlm  21686  qtopuni  21740  tgqtop  21750  isfild  21896  snfil  21902  fbunfip  21907  fgss2  21912  fmco  21999  fbflim2  22015  cnpflf2  22038  fcfelbas  22074  fcfneii  22075  alexsubALTlem2  22086  alexsubALT  22089  tgpconncompeqg  22149  tsmscl  22172  tngngpim  22697  tgioo  22833  xrsmopn  22849  iccntr  22858  reconnlem2  22864  addcnlem  22901  htpycn  23006  phtpyhtpy  23015  pi1blem  23072  fgcfil  23303  ioombl1lem4  23565  dyadmbl  23604  itg2gt0  23764  ditgneg  23858  dvivthlem1  24008  coeeq2  24235  aannenlem2  24321  sineq0  24511  efif1o  24530  leibpilem1  24904  xrlimcnp  24932  vmacl  25081  efvmacl  25083  vmalelog  25167  dchrelbasd  25201  lgsqr  25313  lgsqrmodndvds  25315  gausslemma2dlem0i  25326  2lgslem2  25357  2lgs  25369  2lgsoddprmlem3  25376  uhgr0vb  26204  umgrupgr  26235  umgrnloopv  26238  umgredgprv  26239  umgrislfupgrlem  26254  umgredg  26271  uspgrushgr  26308  uspgrupgr  26309  usgruspgr  26311  usgredgprvALT  26325  usgrnloopvALT  26331  uhgr2edg  26338  edg0usgr  26384  egrsubgr  26408  0uhgrsubgr  26410  uhgrspansubgrlem  26421  nbgrisvtxOLD  26476  nbuhgr  26478  cusgrsize2inds  26600  cusgrfilem2  26603  vtxdg0v  26620  1loopgrnb0  26649  vtxdginducedm1lem4  26689  wlkvtxeledg  26770  wlkeq  26780  wlkl1loop  26785  wlk1walk  26786  upgrwlkedg  26789  uspgr2wlkeq  26793  wlkv0  26798  wlkonl1iedg  26812  wlkon2n0  26813  wlkp1lem8  26828  wlkp1  26829  lfgrwlkprop  26835  lfgrwlknloop  26837  upgrwlkdvde  26884  spthonepeq  26899  uhgrwkspthlem2  26901  usgr2wlkneq  26903  usgr2trlncl  26907  usgr2trlspth  26908  pthdlem2lem  26914  clwlkcompbp  26929  uspgrn2crct  26952  wwlks  26979  wwlknbp  26986  0enwwlksnge1  27014  wwlkswwlksn  27015  wlklnwwlkln1  27018  wwlksnextproplem3  27072  wwlksnextprop  27073  wspthsnonn0vne  27080  wspn0  27087  2pthon3v  27106  umgr2adedgspth  27111  rusgr0edg  27138  clwwlknclwwlkdifsOLD  27145  clwwlkccat  27156  clwlkclwwlklem2fv2  27162  clwlkclwwlklem2a4  27163  clwlkclwwlklem2  27166  clwlkclwwlkflem  27170  clwwlknp  27208  clwwlkwwlksb  27227  clwwlkext2edg  27229  erclwwlkneqlen  27242  hashecclwwlkn1  27251  umgrhashecclwwlk  27252  clwlksfclwwlkOLD  27259  clwlksf1clwwlklemOLD  27265  clwwlknonwwlknonb  27297  upgr1wlkdlem1  27341  upgr3v3e3cycl  27376  uhgr3cyclexlem  27377  1conngr  27390  conngrv2edg  27391  eupth2lem3lem4  27427  eulercrct  27438  frgrusgrfrcond  27457  frgr3vlem2  27472  1to2vfriswmgr  27477  1to3vfriswmgr  27478  frgrncvvdeqlem9  27505  frgrwopreg  27521  frgr2wwlkeqm  27529  2wspmdisj  27535  numclwwlk1lem2f  27557  frgrreggt1  27604  frgrregord013  27606  frgrregord13  27607  l2p  27685  nmlno0lem  27999  normgt0  28335  ocin  28506  nmlnop0iALT  29205  nmopun  29224  cvpss  29495  cvnbtwn  29496  atcvati  29596  mdsymlem6  29618  issgon  30534  mbfmcnt  30678  ballotlemfc0  30902  ballotlemfcc  30903  mthmblem  31822  soasym  32001  sltintdifex  32157  sltres  32158  nosepnelem  32173  nolt02o  32188  pprodss4v  32334  funpartfun  32393  funpartfv  32395  5segofs  32456  btwnxfr  32506  brofs2  32527  brifs2  32528  btwnconn1  32551  segleantisym  32565  broutsideof2  32572  outsidene1  32573  outsidene2  32574  funray  32590  lineunray  32597  cldbnd  32664  bj-dtru  33130  bj-ismoored0  33391  topdifinffinlem  33530  isbasisrelowllem1  33538  isbasisrelowllem2  33539  relowlpssretop  33547  matunitlindf  33739  poimir  33774  volsupnfl  33786  itg2addnclem  33792  cover2  33839  sdclem2  33868  fdc  33871  sstotbnd3  33905  heibor1  33939  clmgmOLD  33980  smgrpmgm  33993  smgrpassOLD  33994  dvrunz  34083  0rngo  34156  lsatcvat  34849  lshpkrex  34917  cmtbr3N  35053  atn0  35107  atnle  35116  cvlsupr4  35144  cvlsupr5  35145  cvlsupr6  35146  cvrval4N  35213  cvratlem  35220  2llnjN  35366  2lplnj  35419  linepsubN  35551  elpaddatiN  35604  elpcliN  35692  pclcmpatN  35700  ldilval  35912  ltrnu  35920  cdleme18d  36094  tendotp  36560  tendof  36562  tendovalco  36564  diatrl  36843  diaintclN  36857  dvheveccl  36911  dibintclN  36966  dihord6apre  37055  dihmeetlem1N  37089  dihpN  37135  dihintcl  37143  dochkrshp4  37188  pw2f1ocnv  38123  iocinico  38315  expgrowthi  39050  iotavalsb  39151  bi23imp1  39217  ioogtlb  40219  iocgtlb  40226  iocleub  40227  icoltub  40233  iooltub  40235  stoweidlem31  40745  funressnfv  41680  2reu2  41717  eu2ndop1stv  41732  afvelrnb0  41771  otiunsndisjX  41887  el1fzopredsuc  41928  fzoopth  41930  2ffzoeq  41931  iccpartimp  41946  iccpartrn  41959  iccpartf  41960  iccpartnel  41967  fargshiftf  41969  fargshiftfo  41971  pfxsuff1eqwrdeq  42000  fmtnofac1  42075  prmdvdsfmtnof1lem2  42090  31prm  42105  lighneallem3  42117  nn0o1gt2ALTV  42198  nn0oALTV  42200  odd2prm2  42220  mogoldbblem  42222  sbgoldbaltlem1  42260  nnsum3primesle9  42275  bgoldbtbndlem1  42286  bgoldbtbndlem2  42287  upwlkbprop  42305  sprel  42320  sprsymrelfvlem  42326  sprsymrelfolem2  42329  mgmpropd  42361  clcllaw  42413  intop  42425  assintop  42431  assintopcllaw  42434  rngimf1o  42491  rngimrnghm  42492  c0snmgmhm  42500  elrngchom  42554  rnghmsubcsetclem1  42561  rnghmsubcsetclem2  42562  rngcid  42565  rngcinv  42567  rngciso  42568  elrngchomALTV  42572  rngccatidALTV  42575  rngcinvALTV  42579  rngcisoALTV  42580  funcrngcsetcALT  42585  zrinitorngc  42586  zrtermorngc  42587  elringchom  42600  rhmsubcsetclem1  42607  rhmsubcsetclem2  42608  ringcid  42611  rhmsubcrngclem1  42613  rhmsubcrngclem2  42614  ringcinv  42618  ringciso  42619  funcringcsetcALTV2lem7  42628  elringchomALTV  42635  ringccatidALTV  42638  ringcinvALTV  42642  ringcisoALTV  42643  funcringcsetclem7ALTV  42651  irinitoringc  42655  zrtermoringc  42656  rhmsubclem3  42674  rhmsubclem4  42675  rhmsubcALTVlem3  42692  rhmsubcALTVlem4  42693  ztprmneprm  42711  suppmptcfin  42746  linccl  42789  linc1  42800  lincolss  42809  ldepspr  42848  nn0sumshdiglem1  43001
  Copyright terms: Public domain W3C validator