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

Theorem syl6bi 232
Description: A mixed syllogism inference. (Contributed by NM, 2-Jan-1994.)
Hypotheses
Ref Expression
syl6bi.1  |-  ( ph  ->  ( ps  <->  ch )
)
syl6bi.2  |-  ( ch 
->  th )
Assertion
Ref Expression
syl6bi  |-  ( ph  ->  ( ps  ->  th )
)

Proof of Theorem syl6bi
StepHypRef Expression
1 syl6bi.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21biimpd 211 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 syl6bi.2 . 2  |-  ( ch 
->  th )
42, 3syl6 34 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188
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 189
This theorem is referenced by:  ax12i  1795  sb3  2185  2eu2  2382  rgen2aOLD  2815  reu6  3226  sseq0  3765  disjel  3810  disjpss  3814  uneqdifeq  3855  preq12b  4150  prel12  4151  prneimg  4155  elinti  4242  zfrepclf  4520  dtru  4593  opth1g  4677  otsndisj  4705  otiunsndisj  4706  elreldm  5058  issref  5212  relcnvtr  5354  relresfld  5361  ordtr2  5466  nsuceq0  5502  ordssun  5521  ordequn  5522  funopg  5613  funimass2  5655  f0dom0  5765  fveqdmss  6015  eldmrexrnb  6027  fvcofneq  6028  fconstfvOLD  6125  elunirn  6154  oprabid  6315  limuni3  6676  peano5  6713  op1steq  6832  bropopvvv  6871  bropfvvvv  6873  f1o2ndf1  6901  frxp  6903  fnwelem  6908  suppimacnv  6922  fvn0elsuppb  6929  suppfnss  6937  reldmtpos  6978  rntpos  6983  seqomlem2  7165  oaordi  7244  oa00  7257  oalimcl  7258  omeulem1  7280  nnaordi  7316  ecopovtrn  7463  undifixp  7555  mapdom2  7740  unxpdomlem3  7775  enp1i  7803  findcard2  7808  infssuni  7862  wdompwdom  8090  opthreg  8120  inf3lemd  8129  inf3lem2  8131  inf3lem6  8135  cnfcomlem  8201  cnfcom3  8206  karden  8363  carden2a  8397  alephdom  8509  dfac5lem4  8554  dfac12r  8573  kmlem2  8578  kmlem12  8588  cfslb2n  8695  alephsing  8703  fin23lem30  8769  fin1a2lem6  8832  fin1a2lem13  8839  axcc2lem  8863  domtriomlem  8869  axdc3lem2  8878  axdc4lem  8882  brdom6disj  8957  alephexp1  9001  pwfseq  9086  addnidpi  9323  indpi  9329  nqereu  9351  ltsonq  9391  distrlem5pr  9449  addcanpr  9468  suplem1pr  9474  suplem2pr  9475  ltsrpr  9498  ltsosr  9515  sqgt0sr  9527  leltne  9720  ltnsym  9729  ltlen  9732  eqlei  9741  eqlei2  9742  infm3  10565  nnunb  10862  0mnnnnn0  10899  elnnnn0b  10911  nn0ge2m1nn  10931  btwnz  11034  uz11  11178  zq  11267  xrleltne  11441  xltnegi  11506  xmulasslem2  11565  reltxrnmnf  11629  icogelb  11683  iccleub  11687  uznfz  11874  2ffzeq  11907  elfzonlteqm1  11986  elfznelfzob  12012  injresinjlem  12021  injresinj  12022  fleqceilz  12078  modadd1  12131  modmul1  12140  modirr  12157  uzrdgfni  12169  fsuppmapnn0fiub0  12202  fsuppmapnn0ub  12204  seqf1o  12251  hashrabsn01  12549  hashrabsn1  12550  hash1snb  12590  hashf1lem2  12616  hash2prde  12628  hash2prd  12631  hash2pwpr  12632  hashge2el2dif  12634  hashge2el2difr  12635  ffz0iswrd  12691  2swrd1eqwrdeq  12805  wrdind  12828  wrd2ind  12829  swrdccatin1  12834  swrdccat3blem  12846  2cshwcshw  12919  cshwcsh2id  12922  wrd2pr2op  13015  2swrd2eqwrdeq  13021  wwlktovf  13024  wwlktovfo  13026  relexpindlem  13119  rexico  13409  lo1le  13708  fsum2dlem  13824  ntrivcvg  13946  fprodss  13995  fprod2dlem  14027  0dvds  14316  gcdneg  14483  algcvga  14531  eucalglt  14537  lcmf  14599  opoe  14754  omoe  14755  opeo  14756  omeo  14757  pockthi  14844  prmreclem5  14857  ramtcl2  14959  ramtcl2OLD  14960  cshwrepswhash1  15066  f1ocpbl  15424  f1ovscpbl  15425  f1olecpbl  15426  monhom  15633  epihom  15640  inveq  15672  invcoisoid  15690  isocoinvid  15691  ciclcl  15700  cicrcl  15701  isinitoi  15891  istermoi  15892  2initoinv  15898  2termoinv  15905  setciso  15979  embedsetcestrclem  16035  ipopos  16399  gsumval2a  16515  ismnddef  16531  symg2bas  17032  symgfix2  17050  gsmsymgreq  17066  pmtrdifellem4  17113  mndodcongi  17185  pj1eu  17339  dprd2da  17668  rimf1o  17955  rimrhm  17956  brric2  17966  lspdisjb  18342  lspsnsubn0  18356  0ring01eq  18488  psrbaglefi  18589  obs2ss  19285  mamufacex  19407  mat0dim0  19485  mat0dimid  19486  mat0dimscm  19487  dmatmat  19512  scmatmat  19527  mat1scmat  19557  1mavmul  19566  mavmulsolcl  19569  gsummatr01  19677  cpmatpmat  19727  cpmadugsumlemF  19893  tg2  19973  unitgOLD  19976  tgcl  19978  neii1  20115  neii2  20117  neindisj2  20132  perfopn  20194  ordtbas2  20200  pnfnei  20229  mnfnei  20230  llyidm  20496  txlm  20656  qtopuni  20710  tgqtop  20720  isfild  20866  snfil  20872  fbunfip  20877  fgss2  20882  fmco  20969  fbflim2  20985  cnpflf2  21008  fcfelbas  21044  fcfneii  21045  alexsubALTlem2  21056  alexsubALT  21059  tgpconcompeqg  21119  tsmscl  21142  tgioo  21807  xrsmopn  21823  iccntr  21832  reconnlem2  21838  addcnlem  21889  htpycn  21997  phtpyhtpy  22006  pi1blem  22063  fgcfil  22234  ioombl1lem4  22507  dyadmbl  22551  itg2gt0  22711  ditgneg  22805  dvivthlem1  22953  coeeq2  23189  aannenlem2  23278  sineq0  23469  efif1o  23488  leibpilem1  23859  xrlimcnp  23887  vmacl  24038  efvmacl  24040  vmalelog  24126  dchrelbasd  24160  lgsqr  24267  uhgra0v  25030  umisuhgra  25047  uslisushgra  25083  uslisumgra  25084  usisuslgra  25085  usgra0v  25091  usgraedgprv  25096  usgra2edg  25102  usgrarnedg  25104  usgraedg4  25107  usgra1v  25110  usgrafisindb0  25129  usgrafisindb1  25130  nbgra0nb  25150  nbcusgra  25184  cusgrasize2inds  25198  cusgrafilem2  25201  usgrasscusgra  25204  uvtxisvtx  25211  2mwlk  25242  wlkcpr  25250  edgwlk  25252  usgrwlknloop  25286  pthistrl  25295  spthonepeq  25310  wlkdvspthlem  25330  usgra2adedgspthlem2  25333  usgra2adedgwlkonALT  25337  usgra2wlkspthlem1  25340  usgra2wlkspthlem2  25341  usgra2wlkspth  25342  crctistrl  25349  cyclispth  25350  cyclispthon  25354  fargshiftf  25357  fargshiftfo  25359  usgrcyclnl2  25362  3v3e3cycl1  25365  constr3trllem2  25372  4cycl4v4e  25387  4cycl4dv  25388  4cycl4dv4e  25389  wwlknimp  25408  wwlkiswwlkn  25423  2wlkeq  25428  usg2wlkeq  25429  wwlkextproplem3  25464  wwlkextprop  25465  clwwlkprop  25491  clwwlkgt0  25492  clwwlknprop  25493  clwwlknimp  25497  clwlkisclwwlklem2fv2  25504  clwlkisclwwlklem2a4  25505  clwlkisclwwlklem1  25508  clwwlkisclwwlkn  25512  clwwlkext2edg  25523  hashecclwwlkn1  25555  usghashecclwwlk  25556  clwlkf1clwwlklem  25570  el2wlkonotlem  25583  el2wlkonot  25590  el2wlkonotot0  25593  2wlkonot3v  25596  2spthonot3v  25597  el2wlksotot  25603  usg2wlkonot  25604  2spontn0vne  25608  vdgr1a  25627  hashnbgravdg  25634  0eusgraiff0rgracl  25662  rusgrasn  25666  rusgra0edg  25676  clwlknclwlkdifs  25681  frgra3vlem2  25722  1to2vfriswmgra  25727  1to3vfriswmgra  25728  vdfrgra0  25743  vdn0frgrav2  25744  vdgn0frgrav2  25745  frgrancvvdeqlem2  25752  frgrancvvdeqlem4  25754  frgrancvvdeqlemC  25760  usgreghash2spotv  25787  frgregordn0  25791  numclwwlkovf2ex  25807  numclwlk1lem2f1  25815  frgrareggt1  25837  frgrareg  25838  frgraregord013  25839  frgraregord13  25840  clmgmOLD  26042  smgrpmgm  26056  smgrpassOLD  26057  dvrunz  26154  nmlno0lem  26427  normgt0  26773  ocin  26942  nmlnop0iALT  27641  nmopun  27660  cvpss  27931  cvnbtwn  27932  atcvati  28032  mdsymlem6  28054  ifbieq12d2  28152  issgon  28938  mbfmcnt  29083  ballotlemfc0  29318  ballotlemfcc  29319  mthmblem  30211  dfres3  30392  sltsgn1  30541  sltsgn2  30542  sltintdifex  30543  sltres  30544  pprodss4v  30644  funpartfun  30703  funpartfv  30705  5segofs  30766  btwnxfr  30816  brofs2  30837  brifs2  30838  btwnconn1  30861  segleantisym  30875  broutsideof2  30882  outsidene1  30883  outsidene2  30884  funray  30900  lineunray  30907  cldbnd  30975  bj-ax12iOLD  31221  bj-sb3v  31361  bj-dtru  31405  topdifinffinlem  31743  isbasisrelowllem1  31751  isbasisrelowllem2  31752  relowlpssretop  31760  poimir  31966  volsupnfl  31978  itg2addnclem  31986  cover2  32033  sdclem2  32064  fdc  32067  sstotbnd3  32101  heibor1  32135  0rngo  32253  lsatcvat  32610  lshpkrex  32678  cmtbr3N  32814  atn0  32868  atnle  32877  cvlsupr4  32905  cvlsupr5  32906  cvlsupr6  32907  cvrval4N  32973  cvratlem  32980  2llnjN  33126  2lplnj  33179  linepsubN  33311  elpaddatiN  33364  elpcliN  33452  pclcmpatN  33460  ldilval  33672  ltrnu  33680  cdleme18d  33855  tendotp  34322  tendof  34324  tendovalco  34326  diatrl  34606  diaintclN  34620  dvheveccl  34674  dibintclN  34729  dihord6apre  34818  dihmeetlem1N  34852  dihpN  34898  dihintcl  34906  dochkrshp4  34951  pw2f1ocnv  35886  iocinico  36090  expgrowthi  36676  iotavalsb  36778  bi23imp1  36845  ioogtlb  37586  iocgtlb  37593  iocleub  37594  icoltub  37601  iooltub  37604  stoweidlem31  37886  2reu2  38602  eu2ndop1stv  38617  funressnfv  38623  afvelrnb0  38660  el1fzopredsuc  38716  mod2eq1n2dvds  38719  iccpartimp  38725  iccpartrn  38738  iccpartf  38739  iccpartnel  38746  nn0o1gt2ALTV  38817  nn0oALTV  38819  sgoldbaltlem1  38874  nnsum3primesle9  38883  bgoldbtbndlem1  38894  bgoldbtbndlem2  38895  pfxsuff1eqwrdeq  38942  propeqop  38993  iunopeqop  38999  otiunsndisjX  39000  2f1fvneq  39008  funopsn  39012  funsndifnop  39016  fundmge2nop  39020  fzoopth  39050  2ffzoeq  39051  hash1n0  39055  xnn0xadd0  39074  uhgr0vb  39151  umgrupgr  39178  umgrnloopv  39180  umgredgprv  39181  umgredg  39215  uspgrushgr  39248  uspgrupgr  39249  usgruspgr  39251  usgredgprvALT  39264  usgrnloopvALT  39270  usgr2edg  39277  edg0usgr  39311  usgr1vr  39312  egrsubgr  39332  0uhgrsubgr  39334  uhgrspansubgrlem  39345  nbuhgr  39394  nbgrisvtx  39410  uvtxaisvtx  39444  vtxnbuvtx  39446  cusgrsize2inds  39497  cusgrfilem2  39500  vtxdg0v  39516  uspgrloopnb0  39539  1wlkv  39613  wlkbProp  39615  2m1wlk  39616  1wlkvtxiedg  39620  1wlk1walk  39630  spthdifv  39653  uhg0v  39676  usgvincvad  39703  usgvincvadALT  39706  usgo0s0  39734  usgo0s0ALT  39735  usgo1s0ALT  39736  usgo1s0  39741  usgfis  39745  usgfisALT  39749  mgmpropd  39762  clcllaw  39814  intop  39826  assintop  39832  assintopcllaw  39835  rngimf1o  39892  rngimrnghm  39893  c0snmgmhm  39901  elrngchom  39957  rnghmsubcsetclem1  39964  rnghmsubcsetclem2  39965  rngcid  39968  rngcinv  39970  rngciso  39971  elrngchomALTV  39975  rngccatidALTV  39978  rngcinvALTV  39982  rngcisoALTV  39983  funcrngcsetcALT  39988  zrinitorngc  39989  zrtermorngc  39990  elringchom  40003  rhmsubcsetclem1  40010  rhmsubcsetclem2  40011  ringcid  40014  rhmsubcrngclem1  40016  rhmsubcrngclem2  40017  ringcinv  40021  ringciso  40022  funcringcsetcALTV2lem7  40031  elringchomALTV  40038  ringccatidALTV  40041  ringcinvALTV  40045  ringcisoALTV  40046  funcringcsetclem7ALTV  40054  irinitoringc  40058  zrtermoringc  40059  rhmsubclem3  40077  rhmsubclem4  40078  rhmsubcALTVlem3  40096  rhmsubcALTVlem4  40097  ztprmneprm  40115  nn0le2is012  40135  suppmptcfin  40151  linccl  40194  linc1  40205  lincolss  40214  ldepspr  40253  nn0o1gt2  40314  nn0sumshdiglem1  40419
  Copyright terms: Public domain W3C validator