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

Theorem syl6bi 241
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 217 . 2 (𝜑 → (𝜓𝜒))
3 syl6bi.2 . 2 (𝜒𝜃)
42, 3syl6 34 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:  ax12i  1864  sb3  2338  2eu2  2537  reu6  3357  sseq0  3922  disjel  3970  disjpss  3975  uneqdifeqOLD  4005  preq12b  4313  prel12  4314  prneimg  4319  elinti  4410  zfrepclf  4695  dtru  4774  opth1g  4863  otsndisj  4891  otiunsndisj  4892  elreldm  5254  issref  5411  relcnvtr  5554  relresfld  5561  ordtr2  5667  ordssun  5726  funopg  5818  funimass2  5868  f0dom0  5983  elfv2ex  6120  fveqdmss  6243  eldmrexrnb  6255  fvcofneq  6256  elunirn  6387  oprabid  6550  brfvopab  6572  limuni3  6917  peano5  6954  op1steq  7074  el2mpt2csbcl  7110  bropopvvv  7115  bropfvvvv  7117  f1o2ndf1  7145  frxp  7147  fnwelem  7152  suppimacnv  7166  fvn0elsuppb  7172  suppfnss  7180  reldmtpos  7220  rntpos  7225  seqomlem2  7406  oaordi  7486  oa00  7499  oalimcl  7500  omeulem1  7522  nnaordi  7558  ecopovtrn  7710  undifixp  7803  mapdom2  7989  unxpdomlem3  8024  enp1i  8053  findcard2  8058  infssuni  8113  wdompwdom  8339  opthreg  8371  inf3lemd  8380  inf3lem2  8382  inf3lem6  8386  cnfcomlem  8452  cnfcom3  8457  karden  8614  carden2a  8648  alephdom  8760  dfac5lem4  8805  dfac12r  8824  kmlem2  8829  kmlem12  8839  cfslb2n  8946  alephsing  8954  fin23lem30  9020  fin1a2lem6  9083  fin1a2lem13  9090  axcc2lem  9114  domtriomlem  9120  axdc3lem2  9129  axdc4lem  9133  brdom6disj  9208  alephexp1  9253  pwfseq  9338  addnidpi  9575  indpi  9581  nqereu  9603  ltsonq  9643  distrlem5pr  9701  addcanpr  9720  suplem1pr  9726  suplem2pr  9727  ltsrpr  9750  ltsosr  9767  sqgt0sr  9779  leltne  9974  ltnsym  9982  ltlen  9985  eqlei  9994  eqlei2  9995  infm3  10827  nnunb  11131  0mnnnnn0  11168  elnnnn0b  11180  nn0ge2m1nn  11203  btwnz  11307  uz11  11538  zq  11622  xrleltne  11809  xltnegi  11876  xmulasslem2  11937  reltxrnmnf  11995  icogelb  12048  iccleub  12052  uznfz  12243  2ffzeq  12280  elfzonlteqm1  12361  elfznelfzob  12391  injresinjlem  12401  injresinj  12402  fleqceilz  12466  modadd1  12520  modmul1  12536  modirr  12554  addmodlteq  12558  uzrdgfni  12570  fsuppmapnn0fiub0  12606  fsuppmapnn0ub  12608  seqf1o  12655  hashrabsn01  12971  hashrabsn1  12972  hash1snb  13016  hashf1lem2  13045  hash2prde  13057  hash2prd  13060  hash2pwpr  13061  hashge2el2dif  13063  hashge2el2difr  13064  ffz0iswrd  13129  ccatrcl1  13171  2swrd1eqwrdeq  13248  wrdind  13270  wrd2ind  13271  swrdccatin1  13276  swrdccat3blem  13288  2cshwcshw  13364  cshwcsh2id  13367  cshimadifsn  13368  2swrd2eqwrdeq  13486  wwlktovf  13489  wwlktovfo  13491  s3sndisj  13496  s3iunsndisj  13497  relexpindlem  13593  rexico  13883  lo1le  14172  fsum2dlem  14285  ntrivcvg  14410  fprodss  14459  fprod2dlem  14491  0dvds  14782  zeneo  14843  mod2eq1n2dvds  14851  opoe  14867  omoe  14868  opeo  14869  omeo  14870  m1exp1  14873  nn0o1gt2  14877  gcdneg  15023  dfgcd2  15043  algcvga  15072  eucalglt  15078  lcmf  15126  coprmdvds  15146  divgcdcoprmex  15160  cncongr1  15161  prm2orodd  15184  prm23lt5  15299  pockthi  15391  prmreclem5  15404  ramtcl2  15495  cshwrepswhash1  15589  f1ocpbl  15950  f1ovscpbl  15951  f1olecpbl  15952  monhom  16160  epihom  16167  inveq  16199  invcoisoid  16217  isocoinvid  16218  ciclcl  16227  cicrcl  16228  isinitoi  16418  istermoi  16419  2initoinv  16425  2termoinv  16432  setciso  16506  embedsetcestrclem  16562  ipopos  16925  gsumval2a  17044  ismnddef  17061  dfgrp2e  17213  symg2bas  17583  symgfix2  17601  gsmsymgreq  17617  pmtrdifellem4  17664  mndodcongi  17727  pj1eu  17874  dprd2da  18206  rimf1o  18499  rimrhm  18500  brric2  18510  lmodfopnelem1  18664  lspdisjb  18889  lspsnsubn0  18903  0ring01eq  19034  psrbaglefi  19135  obs2ss  19830  mamufacex  19952  mat0dim0  20030  mat0dimid  20031  mat0dimscm  20032  dmatmat  20057  scmatmat  20072  mat1scmat  20102  1mavmul  20111  mavmulsolcl  20114  gsummatr01  20222  cpmatpmat  20272  cpmadugsumlemF  20438  tg2  20518  tgcl  20522  neii1  20658  neii2  20660  neindisj2  20675  perfopn  20737  ordtbas2  20743  pnfnei  20772  mnfnei  20773  llyidm  21039  txlm  21199  qtopuni  21253  tgqtop  21263  isfild  21410  snfil  21416  fbunfip  21421  fgss2  21426  fmco  21513  fbflim2  21529  cnpflf2  21552  fcfelbas  21588  fcfneii  21589  alexsubALTlem2  21600  alexsubALT  21603  tgpconcompeqg  21663  tsmscl  21686  tgioo  22335  xrsmopn  22351  iccntr  22360  reconnlem2  22366  addcnlem  22402  htpycn  22507  phtpyhtpy  22516  pi1blem  22574  fgcfil  22791  ioombl1lem4  23049  dyadmbl  23087  itg2gt0  23246  ditgneg  23340  dvivthlem1  23488  coeeq2  23715  aannenlem2  23801  sineq0  23990  efif1o  24009  leibpilem1  24380  xrlimcnp  24408  vmacl  24557  efvmacl  24559  vmalelog  24643  dchrelbasd  24677  lgsqr  24789  gausslemma2dlem0i  24802  2lgslem2  24833  2lgs  24845  2lgsoddprmlem3  24852  uhgra0v  25601  umisuhgra  25618  uslisushgra  25654  uslisumgra  25655  usisuslgra  25656  usgra0v  25662  usgraedgprv  25667  usgra2edg  25673  usgrarnedg  25675  usgraedg4  25678  usgra1v  25681  usgrafisindb0  25699  usgrafisindb1  25700  nbgra0nb  25720  nbcusgra  25754  cusgrasize2inds  25767  cusgrafilem2  25770  usgrasscusgra  25773  uvtxisvtx  25780  2mwlk  25811  wlkcpr  25819  edgwlk  25821  usgrwlknloop  25855  pthistrl  25864  spthonepeq  25879  wlkdvspthlem  25899  usgra2adedgspthlem2  25902  usgra2adedgwlkonALT  25906  usgra2wlkspthlem1  25909  usgra2wlkspthlem2  25910  usgra2wlkspth  25911  crctistrl  25918  cyclispth  25919  cyclispthon  25923  fargshiftf  25926  fargshiftfo  25928  usgrcyclnl2  25931  3v3e3cycl1  25934  constr3trllem2  25941  4cycl4v4e  25956  4cycl4dv  25957  4cycl4dv4e  25958  wwlknimp  25977  wwlkiswwlkn  25992  2wlkeq  25997  usg2wlkeq  25998  wwlkextproplem3  26033  wwlkextprop  26034  clwwlkprop  26060  clwwlkgt0  26061  clwwlknprop  26062  clwwlknimp  26066  clwlkisclwwlklem2fv2  26073  clwlkisclwwlklem2a4  26074  clwlkisclwwlklem1  26077  clwwlkisclwwlkn  26081  clwwlkext2edg  26092  hashecclwwlkn1  26123  usghashecclwwlk  26124  clwlkf1clwwlklem  26138  el2wlkonotlem  26151  el2wlkonot  26158  el2wlkonotot0  26161  2wlkonot3v  26164  2spthonot3v  26165  el2wlksotot  26171  usg2wlkonot  26172  2spontn0vne  26176  vdgr1a  26195  hashnbgravdg  26202  0eusgraiff0rgracl  26230  rusgrasn  26234  rusgra0edg  26244  clwlknclwlkdifs  26249  frgra3vlem2  26290  1to2vfriswmgra  26295  1to3vfriswmgra  26296  vdfrgra0  26311  vdn0frgrav2  26312  vdgn0frgrav2  26313  frgrancvvdeqlem2  26320  frgrancvvdeqlem4  26322  frgrancvvdeqlemC  26328  usgreghash2spotv  26355  frgregordn0  26359  numclwwlkovf2ex  26375  numclwlk1lem2f1  26383  frgrareggt1  26405  frgrareg  26406  frgraregord013  26407  frgraregord13  26408  nmlno0lem  26834  normgt0  27170  ocin  27341  nmlnop0iALT  28040  nmopun  28059  cvpss  28330  cvnbtwn  28331  atcvati  28431  mdsymlem6  28453  issgon  29315  mbfmcnt  29459  ballotlemfc0  29683  ballotlemfcc  29684  mthmblem  30533  dfres3  30704  sltsgn1  30860  sltsgn2  30861  sltintdifex  30862  sltres  30863  pprodss4v  30963  funpartfun  31022  funpartfv  31024  5segofs  31085  btwnxfr  31135  brofs2  31156  brifs2  31157  btwnconn1  31180  segleantisym  31194  broutsideof2  31201  outsidene1  31202  outsidene2  31203  funray  31219  lineunray  31226  cldbnd  31293  bj-ax12iOLD  31606  bj-sb3v  31749  bj-dtru  31794  topdifinffinlem  32170  isbasisrelowllem1  32178  isbasisrelowllem2  32179  relowlpssretop  32187  matunitlindf  32376  poimir  32411  volsupnfl  32423  itg2addnclem  32430  cover2  32477  sdclem2  32507  fdc  32510  sstotbnd3  32544  heibor1  32578  clmgmOLD  32619  smgrpmgm  32632  smgrpassOLD  32633  dvrunz  32722  0rngo  32795  lsatcvat  33154  lshpkrex  33222  cmtbr3N  33358  atn0  33412  atnle  33421  cvlsupr4  33449  cvlsupr5  33450  cvlsupr6  33451  cvrval4N  33517  cvratlem  33524  2llnjN  33670  2lplnj  33723  linepsubN  33855  elpaddatiN  33908  elpcliN  33996  pclcmpatN  34004  ldilval  34216  ltrnu  34224  cdleme18d  34399  tendotp  34866  tendof  34868  tendovalco  34870  diatrl  35150  diaintclN  35164  dvheveccl  35218  dibintclN  35273  dihord6apre  35362  dihmeetlem1N  35396  dihpN  35442  dihintcl  35450  dochkrshp4  35495  pw2f1ocnv  36421  iocinico  36615  expgrowthi  37353  iotavalsb  37455  bi23imp1  37521  ioogtlb  38364  iocgtlb  38371  iocleub  38372  icoltub  38379  iooltub  38382  stoweidlem31  38724  2reu2  39636  eu2ndop1stv  39651  funressnfv  39657  afvelrnb0  39694  el1fzopredsuc  39749  iccpartimp  39756  iccpartrn  39769  iccpartf  39770  iccpartnel  39777  fmtnofac1  39821  prmdvdsfmtnof1lem2  39836  31prm  39851  lighneallem3  39863  nn0o1gt2ALTV  39944  nn0oALTV  39946  sgoldbaltlem1  40002  nnsum3primesle9  40011  bgoldbtbndlem1  40022  bgoldbtbndlem2  40023  pfxsuff1eqwrdeq  40071  propeqop  40122  iunopeqop  40127  otiunsndisjX  40128  2f1fvneq  40134  funopsn  40140  funsndifnop  40144  fundmge2nop0  40148  fzoopth  40183  2ffzoeq  40184  elfzr  40187  elfzo0l  40188  elfzlmr  40189  hash1n0  40194  xnn0xadd0  40213  uhgr0vb  40295  umgrupgr  40326  umgrnloopv  40329  umgredgprv  40330  umgrislfupgrlem  40345  umgredg  40369  uspgrushgr  40403  uspgrupgr  40404  usgruspgr  40406  usgredgprvALT  40420  usgrnloopvALT  40426  uhgr2edg  40433  edg0usgr  40477  egrsubgr  40499  0uhgrsubgr  40501  uhgrspansubgrlem  40512  nbuhgr  40563  nbgrisvtx  40579  uvtxaisvtx  40613  vtxnbuvtx  40615  uvtx2vtx1edg  40623  cusgrsize2inds  40667  cusgrfilem2  40670  vtxdg0v  40686  1loopgrnb0  40715  wlkbProp  40815  2m1wlk  40816  1wlkvtxeledg  40826  1wlkeq  40836  1wlkl1loop  40840  1wlk1walk  40841  upgrwlkedg  40848  uspgr2wlkeq  40852  1wlkv0  40857  wlkOnl1iedg  40871  wlkOn2n0  40872  1wlkp1lem8  40887  1wlkp1  40888  lfgrwlkprop  40894  lfgr1wlknloop  40896  trlis1wlk  40903  trlf1  40904  PthisTrl  40929  pthdivtx  40933  spthdep  40938  pthdepissPth  40939  spthonepeq-av  40956  uhgr1wlkspthlem2  40958  usgr2wlkneq  40960  usgr2trlncl  40964  usgr2trlspth  40965  pthdlem2lem  40971  clwlkis1wlk  40979  cyclisPthon  41005  uspgrn2crct  41009  wwlks  41036  wwlknbp  41042  0enwwlksnge1  41058  wwlkswwlksn  41059  1wlklnwwlkln1  41063  wwlksnextproplem3  41115  wwlksnextprop  41116  wspthsnonn0vne  41122  2pthon3v-av  41148  umgr2adedgspth  41153  wwlks2onv  41156  rusgr0edg  41174  clwwlknclwwlkdifs  41179  clwwlknbp0  41190  isclwwlksnx  41195  clwwlkclwwlkn  41197  clwlkclwwlklem2fv2  41203  clwlkclwwlklem2a4  41204  clwlkclwwlklem2  41207  clwwlksext2edg  41228  erclwwlksneqlen  41250  hashecclwwlksn1  41259  umgrhashecclwwlk  41260  clwlksfclwwlk  41267  clwlksf1clwwlklem  41273  upgr11wlkdlem1  41310  upgr3v3e3cycl  41345  uhgr3cyclexlem  41346  1conngr  41359  conngrv2edg  41360  eupth2lem3lem4  41397  eulercrct  41408  frgrusgrfrcond  41429  frgr3vlem2  41442  1to2vfriswmgr  41447  1to3vfriswmgr  41448  frgrncvvdeqlem2  41468  frgrncvvdeqlem4  41470  frgrncvvdeqlemC  41476  fusgreghash2wspv  41497  fusgreg2wsp  41498  frrusgrord0  41501  av-numclwwlkovf2ex  41515  av-numclwlk1lem2f1  41522  av-frgrareggt1  41545  av-frgraregord013  41547  av-frgraregord13  41548  mgmpropd  41563  clcllaw  41615  intop  41627  assintop  41633  assintopcllaw  41636  rngimf1o  41693  rngimrnghm  41694  c0snmgmhm  41702  elrngchom  41758  rnghmsubcsetclem1  41765  rnghmsubcsetclem2  41766  rngcid  41769  rngcinv  41771  rngciso  41772  elrngchomALTV  41776  rngccatidALTV  41779  rngcinvALTV  41783  rngcisoALTV  41784  funcrngcsetcALT  41789  zrinitorngc  41790  zrtermorngc  41791  elringchom  41804  rhmsubcsetclem1  41811  rhmsubcsetclem2  41812  ringcid  41815  rhmsubcrngclem1  41817  rhmsubcrngclem2  41818  ringcinv  41822  ringciso  41823  funcringcsetcALTV2lem7  41832  elringchomALTV  41839  ringccatidALTV  41842  ringcinvALTV  41846  ringcisoALTV  41847  funcringcsetclem7ALTV  41855  irinitoringc  41859  zrtermoringc  41860  rhmsubclem3  41878  rhmsubclem4  41879  rhmsubcALTVlem3  41897  rhmsubcALTVlem4  41898  ztprmneprm  41916  nn0le2is012  41936  suppmptcfin  41952  linccl  41995  linc1  42006  lincolss  42015  ldepspr  42054  nn0sumshdiglem1  42211
  Copyright terms: Public domain W3C validator