MPE Home 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  1960  sb3OLD  2501  sb1OLD  2503  sb4a  2505  hbsb2  2517  dfsb2  2528  2eu2  2734  nfabdw  3000  reu6  3716  2reu2  3881  sseq0  4352  disjel  4404  disjpss  4408  preq12b  4775  prneimg  4779  preqsnd  4783  elinti  4878  zfrepclf  5190  dtru  5263  opth1g  5362  sbcop1  5371  snopeqop  5388  propeqop  5389  otsndisj  5401  otiunsndisj  5402  iunopeqop  5403  po2ne  5483  soasym  5498  elreldm  5799  dfres3  5852  relcnvtrg  6113  relresfld  6121  ordtr2  6229  ordssun  6284  funopg  6383  funimass2  6431  f0dom0  6557  elfv2ex  6705  fveqdmss  6839  eldmrexrnb  6851  fvcofneq  6852  funopsn  6903  funopdmsn  6905  funsndifnop  6906  elunirn  7001  2f1fvneq  7009  oprabidw  7176  oprabid  7177  brfvopab  7200  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  17885  ismnddef  17903  dfgrp2e  18069  symg2bas  18457  symgfix2  18475  gsmsymgreq  18491  pmtrdifellem4  18538  mndodcongi  18602  pj1eu  18753  cycsubmcmn  18939  dprd2da  19095  rimf1o  19417  rimrhm  19418  brric2  19431  lmodfopnelem1  19601  lspdisjb  19829  lspsnsubn0  19843  0ring01eq  19974  psrbaglefi  20082  obs2ss  20803  mamufacex  20930  mat0dim0  21006  mat0dimid  21007  mat0dimscm  21008  dmatmat  21033  scmatmat  21048  mat1scmat  21078  1mavmul  21087  mavmulsolcl  21090  gsummatr01  21198  cpmatpmat  21248  cpmadugsumlemF  21414  tg2  21503  tgcl  21507  neii1  21644  neii2  21646  neindisj2  21661  perfopn  21723  ordtbas2  21729  pnfnei  21758  mnfnei  21759  llyidm  22026  txlm  22186  qtopuni  22240  tgqtop  22250  isfild  22396  snfil  22402  fbunfip  22407  fgss2  22412  fmco  22499  fbflim2  22515  cnpflf2  22538  fcfelbas  22574  fcfneii  22575  alexsubALTlem2  22586  alexsubALT  22589  tgpconncompeqg  22649  tsmscl  22672  tngngpim  23197  tgioo  23333  xrsmopn  23349  iccntr  23358  reconnlem2  23364  addcnlem  23401  htpycn  23506  phtpyhtpy  23515  pi1blem  23572  fgcfil  23803  ioombl1lem4  24091  dyadmbl  24130  itg2gt0  24290  ditgneg  24384  dvivthlem1  24534  coeeq2  24761  aannenlem2  24847  sineq0  25038  efif1o  25057  leibpilem1OLD  25446  xrlimcnp  25474  vmacl  25623  efvmacl  25625  vmalelog  25709  dchrelbasd  25743  lgsqr  25855  lgsqrmodndvds  25857  gausslemma2dlem0i  25868  2lgslem2  25899  2lgs  25911  2lgsoddprmlem3  25918  2sqnn  25943  2sqreultlem  25951  2sqreultblem  25952  2sqreunnltlem  25954  2sqreunnltblem  25955  elntg2  26699  uhgr0vb  26785  umgrupgr  26816  umgrnloopv  26819  umgredgprv  26820  umgrislfupgrlem  26835  umgredg  26851  uspgrushgr  26888  uspgrupgr  26889  usgruspgr  26891  usgredgprvALT  26905  usgrnloopvALT  26911  uhgr2edg  26918  edg0usgr  26963  egrsubgr  26987  0uhgrsubgr  26989  uhgrspansubgrlem  27000  nbuhgr  27053  cusgrsize2inds  27163  cusgrfilem2  27166  vtxdg0v  27183  1loopgrnb0  27212  vtxdginducedm1lem4  27252  wlkvtxeledg  27333  wlkeq  27343  wlkl1loop  27347  wlk1walk  27348  upgrwlkedg  27351  uspgr2wlkeq  27355  wlkv0  27360  wlkonl1iedg  27375  wlkon2n0  27376  wlkp1lem8  27390  wlkp1  27391  lfgrwlkprop  27397  lfgrwlknloop  27399  2pthnloop  27440  upgrwlkdvde  27446  spthonepeq  27461  uhgrwkspthlem2  27463  usgr2wlkneq  27465  usgr2trlncl  27469  usgr2trlspth  27470  pthdlem2lem  27476  clwlkcompbp  27491  uspgrn2crct  27514  wwlks  27541  wwlknbp  27548  0enwwlksnge1  27570  wwlkswwlksn  27571  wlklnwwlkln1  27574  wwlksnextproplem3  27618  wwlksnextprop  27619  wspthsnonn0vne  27624  wspn0  27631  2pthon3v  27650  umgr2adedgspth  27655  rusgr0edg  27680  clwwlkccat  27696  clwlkclwwlklem2fv2  27702  clwlkclwwlklem2a4  27703  clwlkclwwlklem2  27706  clwlkclwwlkflem  27710  clwwlknp  27743  clwwlkwwlksb  27761  clwwlkext2edg  27763  erclwwlkneqlen  27775  hashecclwwlkn1  27784  umgrhashecclwwlk  27785  clwwlknonwwlknonb  27813  upgr1wlkdlem1  27852  upgr3v3e3cycl  27887  uhgr3cyclexlem  27888  1conngr  27901  conngrv2edg  27902  eupth2lem3lem4  27938  eulercrct  27949  isfrgr  27967  frgr3vlem2  27981  1to2vfriswmgr  27986  1to3vfriswmgr  27987  frgrncvvdeqlem9  28014  frgrwopreg  28030  frgr2wwlkeqm  28038  2wspmdisj  28044  numclwwlk1lem2f  28062  frgrreggt1  28100  frgrregord013  28102  frgrregord13  28103  l2p  28184  nmlno0lem  28498  normgt0  28832  ocin  29001  nmlnop0iALT  29700  nmopun  29719  cvpss  29990  cvnbtwn  29991  atcvati  30091  mdsymlem6  30113  iunrnmptss  30246  wrdt2ind  30555  issgon  31282  mbfmcnt  31426  ballotlemfc0  31650  ballotlemfcc  31651  satfv0  32503  satfv0fun  32516  fmla1  32532  gonarlem  32539  gonar  32540  goalrlem  32541  goalr  32542  fmla0disjsuc  32543  satffunlem  32546  satffunlem1lem1  32547  satffunlem2lem1  32549  satfun  32556  satfv0fvfmla0  32558  sategoelfv  32565  mthmblem  32725  sltintdifex  33066  sltres  33067  nosepnelem  33082  nolt02o  33097  pprodss4v  33243  funpartfun  33302  funpartfv  33304  5segofs  33365  btwnxfr  33415  brofs2  33436  brifs2  33437  btwnconn1  33460  segleantisym  33474  broutsideof2  33481  outsidene1  33482  outsidene2  33483  funray  33499  lineunray  33506  cldbnd  33572  bj-dtru  34037  bj-imdirval3  34367  topdifinffinlem  34511  isbasisrelowllem1  34519  isbasisrelowllem2  34520  relowlpssretop  34528  inunissunidif  34539  pibt2  34581  matunitlindf  34772  poimir  34807  volsupnfl  34819  itg2addnclem  34825  cover2  34872  sdclem2  34900  fdc  34903  sstotbnd3  34937  heibor1  34971  clmgmOLD  35012  smgrpmgm  35025  smgrpassOLD  35026  dvrunz  35115  0rngo  35188  lsatcvat  36068  lshpkrex  36136  cmtbr3N  36272  atn0  36326  atnle  36335  cvlsupr4  36363  cvlsupr5  36364  cvlsupr6  36365  cvrval4N  36432  cvratlem  36439  2llnjN  36585  2lplnj  36638  linepsubN  36770  elpaddatiN  36823  elpcliN  36911  pclcmpatN  36919  ldilval  37131  ltrnu  37139  cdleme18d  37313  tendotp  37779  tendof  37781  tendovalco  37783  diatrl  38062  diaintclN  38076  dvheveccl  38130  dibintclN  38185  dihord6apre  38274  dihmeetlem1N  38308  dihpN  38354  dihintcl  38362  dochkrshp4  38407  oexpreposd  39059  pw2f1ocnv  39514  iocinico  39698  infordmin  39779  pr2cv  39787  expgrowthi  40545  iotavalsb  40645  bi23imp1  40709  ioogtlb  41650  iocgtlb  41657  iocleub  41658  icoltub  41664  iooltub  41666  stoweidlem31  42197  oppr  43146  funressnfv  43159  eu2ndop1stv  43205  afvelrnb0  43244  otiunsndisjX  43359  el1fzopredsuc  43406  fzoopth  43408  2ffzoeq  43409  iccpartimp  43424  iccpartrn  43437  iccpartf  43438  iccpartnel  43445  fargshiftf  43447  fargshiftfo  43449  ichnfim  43471  ichreuopeq  43482  sprel  43493  sprsymrelfvlem  43499  sprsymrelfolem2  43502  prproropf1olem4  43515  prprelb  43525  poprelb  43533  fmtnofac1  43579  prmdvdsfmtnof1lem2  43594  31prm  43607  lighneallem3  43619  nn0o1gt2ALTV  43706  nn0oALTV  43708  odd2prm2  43730  mogoldbblem  43732  fpprbasnn  43741  fpprnn  43742  sbgoldbaltlem1  43791  nnsum3primesle9  43806  bgoldbtbndlem1  43817  bgoldbtbndlem2  43818  isomuspgrlem2d  43843  upwlkbprop  43860  mgmpropd  43889  clcllaw  43996  intop  44008  assintop  44014  assintopcllaw  44017  rngimf1o  44074  rngimrnghm  44075  c0snmgmhm  44083  elrngchom  44137  rnghmsubcsetclem1  44144  rnghmsubcsetclem2  44145  rngcid  44148  rngcinv  44150  rngciso  44151  elrngchomALTV  44155  rngccatidALTV  44158  rngcinvALTV  44162  rngcisoALTV  44163  funcrngcsetcALT  44168  zrinitorngc  44169  zrtermorngc  44170  elringchom  44183  rhmsubcsetclem1  44190  rhmsubcsetclem2  44191  ringcid  44194  rhmsubcrngclem1  44196  rhmsubcrngclem2  44197  ringcinv  44201  ringciso  44202  funcringcsetcALTV2lem7  44211  elringchomALTV  44218  ringccatidALTV  44221  ringcinvALTV  44225  ringcisoALTV  44226  funcringcsetclem7ALTV  44234  irinitoringc  44238  zrtermoringc  44239  rhmsubclem3  44257  rhmsubclem4  44258  rhmsubcALTVlem3  44275  rhmsubcALTVlem4  44276  ztprmneprm  44293  suppmptcfin  44325  linccl  44367  linc1  44378  lincolss  44387  ldepspr  44426  nn0sumshdiglem1  44579  rrxlines  44618  rrxsphere  44633  itsclc0yqsol  44649  itschlc0xyqsol1  44651
  Copyright terms: Public domain W3C validator