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

Theorem syl6bb 252
Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl6bb.1  |-  ( ph  ->  ( ps  <->  ch )
)
syl6bb.2  |-  ( ch  <->  th )
Assertion
Ref Expression
syl6bb  |-  ( ph  ->  ( ps  <->  th )
)

Proof of Theorem syl6bb
StepHypRef Expression
1 syl6bb.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
2 syl6bb.2 . . 3  |-  ( ch  <->  th )
32a1i 10 . 2  |-  ( ph  ->  ( ch  <->  th )
)
41, 3bitrd 244 1  |-  ( ph  ->  ( ps  <->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  syl6rbb  253  syl6bbr  254  3bitr3g  278  bibi2i  304  ibibr  332  pm5.75  903  cadan  1382  19.17  1788  2eu6  2228  abeq2d  2392  necon2bbid  2504  cbvralf  2758  cbvreu  2762  cbvrab  2786  ceqsralt  2811  ralab2  2930  rexab2  2932  reu7  2960  reu8  2961  2reu5  2973  cbvralcsf  3143  cbvreucsf  3145  cbvrabcsf  3146  ralss  3239  rexss  3240  prssg  3770  ssunsn2  3773  eqsn  3775  2ralunsn  3816  eluniab  3839  elintab  3873  dfiun2g  3935  dfiin2g  3936  disjprg  4019  disjxun  4021  cbvopab1  4089  cbvmpt  4110  axsep2  4142  notzfaus  4185  opeqsn  4262  sotrieq2  4342  ordtri2  4427  oneqmini  4443  reusv3  4542  reusv6OLD  4545  reusv7OLD  4546  reuxfrd  4559  elpwunsn  4568  tfisi  4649  frsn  4760  eliunxp  4823  relop  4834  eldm2g  4875  reldm0  4896  relrn0  4937  asymref2  5060  somin1  5079  xpnz  5099  xpcan  5112  xpcan2  5113  cbviota  5224  iota1  5233  sniota  5246  fncnv  5314  fnres  5360  brprcneu  5518  fnopfvb  5564  fvelrnb  5570  funimass4  5573  dffv2  5592  fvopab3g  5598  eqfnfv  5622  eqfnfv3  5624  eqfnfv2f  5626  fvreseq  5628  fnreseql  5635  fniniseg  5646  rexsupp  5650  respreima  5654  rexrn  5667  ralrn  5668  f1ompt  5682  fsn  5696  fconstfv  5734  eufnfv  5752  rexima  5757  ralima  5758  dff13  5783  fliftfun  5811  isocnv  5827  isoini  5835  f1oiso  5848  oprabid  5882  eloprabga  5934  resoprab  5940  eqfnov  5950  eqfnov2  5951  ov6g  5985  ovelrn  5996  funimassov  5997  ovelimab  5998  ndmovg  6003  caovord2  6032  eqop  6162  releldm2  6170  dfoprab4  6177  exopxfr2  6184  fparlem1  6218  fparlem2  6219  xporderlem  6226  poxp  6227  soxp  6228  fnwelem  6230  brtpos2  6240  brtpos0  6241  rntpos  6247  dftpos3  6252  tpostpos  6254  tpossym  6266  tposoprab  6270  opiota  6290  cbvriota  6315  eusvobj2  6337  oevn0  6514  om00el  6574  omordlim  6575  omlimcl  6576  oeoa  6595  oeoe  6597  oeeulem  6599  oeeui  6600  oaabs2  6643  omabs  6645  erth2  6705  qliftfun  6743  erovlem  6754  ecopovsym  6760  th3qlem1  6764  elpmg  6786  elpm2g  6787  map0e  6805  dom2lem  6901  mapsnen  6938  xpdom2  6957  omxpenlem  6963  0sdomg  6990  fodomr  7012  xpf1o  7023  mapen  7025  ac6sfi  7101  marypha2lem3  7190  ordtypelem7  7239  wemaplem1  7261  wemapso2lem  7265  wemapso2  7267  elharval  7277  brwdom3  7296  unwdomg  7298  xpwdomg  7299  inf3lem1  7329  cantnfs  7367  cantnfp1lem2  7381  cantnflem1d  7390  cantnflem1  7391  mapfien  7399  wemapwe  7400  r1sdom  7446  rankr1ai  7470  rankval2  7490  unbndrank  7514  rankunb  7522  tcrank  7554  bnd2  7563  cardnueq0  7597  iscard2  7609  r0weon  7640  fseqenlem1  7651  alephord2  7703  cardaleph  7716  aceq0  7745  dfac5lem4  7753  dfac5  7755  kmlem14  7789  cfsmolem  7896  isfin4-2  7940  fin23lem26  7951  fin23lem22  7953  fin1a2lem7  8032  axdc3lem2  8077  axdc3  8080  zfac  8086  zornn0g  8132  axdclem  8146  brdom3  8153  zfcndac  8241  fpwwe2lem8  8259  fpwwe2lem12  8263  fpwwe2lem13  8264  fpwwe2  8265  pwfseqlem3  8282  winainflem  8315  eltsk2g  8373  inatsk  8400  axgroth2  8447  axgroth6  8450  sstskm  8464  ltexpi  8526  ordpinq  8567  lterpq  8594  ltanq  8595  ltmnq  8596  genpv  8623  genpelv  8624  prlem934  8657  prlem936  8671  addcmpblnr  8694  ltsrpr  8699  ltsosr  8716  mulgt0sr  8727  supsrlem  8733  elreal2  8754  ltresr  8762  ltresr2  8763  axrrecex  8785  axpre-ltadd  8789  axpre-mulgt0  8790  axpre-sup  8791  subcan2  9072  negcon1  9099  negcon2  9100  lt0neg1  9280  lt0neg2  9281  le0neg1  9282  le0neg2  9283  msq0d  9417  divmul2  9428  reclt1  9651  recgt1  9652  fimaxre  9701  infm3  9713  suprlub  9716  suprleub  9718  infmrgelb  9734  addltmul  9947  arch  9962  elznn0  10038  nn0lt10b  10078  recnz  10087  uzindOLD  10106  eluz1  10234  raluz  10267  rexuz  10269  nnwof  10285  cnref1o  10349  ltxr  10457  xrltlen  10480  dflt2  10482  xrrebnd  10497  qbtwnre  10526  xlt0neg1  10546  xlt0neg2  10547  xle0neg1  10548  xle0neg2  10549  xmulneg1  10589  supxrbnd  10647  elixx1  10665  ixxun  10672  elioo2  10697  elicc4  10717  elioopnf  10737  elioomnf  10738  iooneg  10756  iccneg  10757  iccshftr  10769  iccshftl  10771  iccdil  10773  icccntr  10775  iccf1o  10778  elfz1  10787  0fz1  10813  elfzp1  10836  fzpr  10840  fznn0  10851  uzsplit  10855  elfzm1b  10860  elfzp12  10861  fzm1  10862  bernneq  11227  hashbclem  11390  hashfacen  11392  hashf1  11395  2shfti  11575  sqrmsq2i  11871  limsupgle  11951  limsuple  11952  rlim  11969  clim0  11980  ello12  11990  elo12  12001  o1lo1  12011  rlimresb  12039  lo1add  12100  lo1mul  12101  rlimno1  12127  summo  12190  fsumsplit  12212  mertenslem2  12341  xpnnenOLD  12488  cnso  12525  sqr2irr  12527  dvdsval2  12534  alzdvds  12578  odd2np1lem  12586  divalgb  12603  bitsval  12615  bitsmod  12627  sadcp1  12646  gcddvds  12694  bezoutlem3  12719  bezout  12721  isprm3  12767  prmind2  12769  dvdsprime  12771  coprm  12779  prmdvdsexp  12793  crt  12846  pythagtriplem2  12870  pythagtrip  12887  pceu  12899  pc11  12932  vdwapval  13020  vdwapun  13021  vdwlem10  13037  vdwlem12  13039  vdwlem13  13040  ramval  13055  ramub1lem2  13074  prmlem0  13107  elrest  13332  imasleval  13443  ismri  13533  isacs  13553  isacs2  13555  acsfn1  13563  iscatd2  13583  homfeq  13597  catpropd  13612  ismon  13636  issect  13656  issect2  13657  isinv  13662  invsym  13664  isssc  13697  subsubc  13727  isfunc  13738  funcres2b  13771  isnat  13821  fucinv  13847  elhoma  13864  setcinv  13922  isprs  14064  isdrs  14068  istos  14141  tosso  14142  latnle  14191  isipodrs  14264  isacs5  14275  latdisd  14293  isdlat  14296  spwmo  14335  ismhm  14417  issubm  14425  grpsubeq0  14552  grpsubadd  14553  issubg  14621  subgmulg  14635  issubg3  14637  0subg  14642  isnsg  14646  eqger  14667  eqglact  14668  eqgid  14669  isghm  14683  isga  14745  gacan  14759  gaorb  14761  gastacos  14764  orbsta  14767  elcntz  14798  elcntzsn  14801  sscntz  14802  dfod2  14877  isslw  14919  sylow2alem2  14929  lsmelvalx  14951  lsmcom2  14966  lsmass  14979  lssnle  14983  pj1eu  15005  lsmhash  15014  efgi  15028  efgval2  15033  efgtlen  15035  efgred  15057  lsmcomx  15148  iscyggen2  15168  iscyg3  15173  cygabl  15177  gsumval3eu  15190  gsumzsplit  15206  eldprd  15239  subgdmdprd  15269  dprddisj2  15274  dprd2da  15277  dmdprdsplit2lem  15280  dmdprdsplit2  15281  dprdsplit  15283  dmdprdpr  15284  pgpfac1lem3  15312  pgpfac1lem4  15313  pgpfac1lem5  15314  dvdsr02  15438  isunit  15439  isirred  15481  isrhm  15501  drngunit  15517  subsubrg2  15572  issubrg3  15573  isabv  15584  islmod  15631  islss  15692  lsslss  15718  lspsnel  15760  islmhm  15784  lmhmeql  15812  islbs  15829  lsmspsn  15837  lsmelval2  15838  lspprel  15847  lvecvscan2  15865  lvecinv  15866  lspsneq  15875  lspsneu  15876  lspsolvlem  15895  islpidl  15998  lidldvgen  16007  isnzr2  16015  aspval2  16086  mplsubglem  16179  mpllsslem  16180  mplmonmul  16208  opsrtoslem2  16226  prmirredlem  16446  zrhrhmb  16465  zndvds  16503  elocv  16568  iscss  16583  pjdm  16607  ishil2  16619  isobs  16620  obslbs  16630  istop2g  16642  istopon  16663  isbasis2g  16686  isbasis3g  16687  tgss2  16725  bastop1  16731  iscld  16764  elcls  16810  ntreq0  16814  isclo  16824  isclo2  16825  islp  16872  lpdifsn  16875  islpi  16880  restsn  16901  restopn2  16908  restlp  16913  ordtbaslem  16918  ordtbas2  16921  lmbr  16988  cnprest2  17018  ist0-3  17073  ist1-2  17075  cmpsublem  17126  cmpfi  17135  1stcrest  17179  2ndcdisj  17182  1stccnp  17188  llyi  17200  nllyi  17201  lly1stc  17222  iskgen3  17244  kgencn  17251  txbas  17262  eltx  17263  elpt  17267  xkoccn  17313  ptcnplem  17315  hausdiag  17339  hauseqlcld  17340  txlm  17342  txkgen  17346  kqfvima  17421  kqt0lem  17427  r0cld  17429  regr1lem2  17431  hmeoimaf1o  17461  isfbas2  17530  fbssfi  17532  trfbas2  17538  trfil2  17582  fmfnfmlem4  17652  elflim2  17659  flimrest  17678  cnflf  17697  txflf  17701  fclsopn  17709  ufilcmp  17727  cnfcf  17737  alexsubALTlem4  17744  tmdcn2  17772  divstgpopn  17802  divstgplem  17803  eltsms  17815  tsmsgsum  17821  tsmssplit  17834  ismet  17888  isxmet  17889  ismet2  17898  metn0  17924  elbl  17949  metrest  18070  dscmet  18095  nrmmetd  18097  isngp3  18120  nmogelb  18225  isnmhm  18255  qtopbaslem  18267  xrsxmet  18315  icccmplem2  18328  metdseq0  18358  elcncf  18393  cnheibor  18453  ishtpy  18470  isphtpy  18479  isphtpc  18492  om1elbas  18530  elpi1  18543  nmhmcn  18601  iscph  18606  tchcph  18667  lmmbrf  18688  iscfil  18691  iscfil2  18692  iscau  18702  caucfil  18709  iscmet  18710  iscmet3  18719  bcthlem1  18746  minveclem3b  18792  minveclem6  18798  evthicc2  18820  ovolfioo  18827  ovolficc  18828  ovolshftlem1  18868  ovolscalem1  18872  iundisj2  18906  dyadmbl  18955  volsup2  18960  mbfmax  19004  mbfaddlem  19015  mbfsup  19019  mbfinf  19020  i1f1lem  19044  i1fres  19060  itg1climres  19069  mbfi1fseqlem4  19073  itg2leub  19089  itg2seq  19097  itg2splitlem  19103  itg2monolem1  19105  itg2mono  19108  itg2cn  19118  iblpos  19147  iblcn  19153  itgsplit  19190  ellimc2  19227  dvreslem  19259  elcpn  19283  rolle  19337  dvlip  19340  dvivth  19357  tdeglem4  19446  deg1ldg  19478  ply1nzb  19508  ply1divmo  19521  ply1divex  19522  fta1glem2  19552  plyco0  19574  elply  19577  coeeu  19607  plydivex  19677  taylthlem2  19753  radcnvlt1  19794  sincosq1sgn  19866  sincosq2sgn  19867  coseq1  19890  logreclem  20116  affineequiv  20123  dcubic  20142  quart  20157  atans2  20227  efrlim  20264  mumullem2  20418  dvdsflsumcom  20428  fsumvma2  20453  chpchtsum  20458  chpub  20459  dchrelbas  20475  dchrelbas2  20476  dchreq  20497  dchrptlem2  20504  lgsquadlem2  20594  lgsquadlem3  20595  m1lgs  20601  2sqlem6  20608  2sqlem9  20612  2sqlem10  20613  dchrisum0flb  20659  pntpbnd1  20735  pntlem3  20758  pntlemp  20759  isgrpo  20863  isgrpo2  20864  isgrp2d  20902  issubgo  20970  ismgm  20987  rngosn3  21093  nvsubadd  21213  isssp  21300  islno  21331  nmogtmnf  21348  nmoubi  21350  nmounbi  21354  isblo  21360  ishmo  21389  ubthlem1  21449  ubthlem2  21450  minvecolem5  21460  minvecolem6  21461  hvmulcan2  21652  hire  21673  ocel  21860  ocsh  21862  pjhthmo  21881  shscom  21898  shmodsi  21968  elspani  22122  adjsym  22413  eigorthi  22417  nmopgtmnf  22448  adjeu  22469  adjval2  22471  cnvadj  22472  nmopub  22488  nmfnleub  22505  eleigvec  22537  nmop0h  22571  largei  22847  mdbr2  22876  mddmd2  22889  mdsl2i  22902  chrelat3  22951  atnemeq0  22957  chirredlem1  22970  sumdmdii  22995  sumdmdlem  22998  dmdbr5ati  23002  cdjreui  23012  ballotlemodife  23056  preqsnd  23194  cbvmptf  23220  funcnv5mpt  23236  curry2ima  23247  disjabrex  23359  disjabrexf  23360  iundisj2fi  23364  iundisj2f  23366  mbfmcnt  23573  dya2iocrrnval  23582  isibfm  23593  ind1a  23604  elorvc  23660  subfacp1lem3  23713  subfacp1lem5  23715  subfacp1lem6  23716  erdszelem9  23730  erdszelem10  23731  erdsze2lem2  23735  iscvm  23790  cvmlift2lem10  23843  wrdumgra  23868  eupath2lem2  23902  eupath2lem3  23903  snmlval  23914  elgiso  24003  climuzcnv  24004  zmodid2  24010  mulcan2g  24085  mulsuble0b  24088  pdivsq  24102  dfpo2  24112  br6  24114  fprb  24129  dfdm5  24132  dfrn5  24133  dfon2lem7  24145  dfon2  24148  dfrdg2  24152  predreseq  24179  wfrlem1  24256  frrlem1  24281  sltval2  24310  sltintdifex  24317  sltres  24318  nofulllem5  24360  dfiota3  24462  brimg  24476  brsuccf  24480  dfrdg4  24488  elee  24522  mptelee  24523  colinearalglem2  24535  colinearalg  24538  ax5seglem5  24561  axeuclidlem  24590  axeuclid  24591  axcontlem1  24592  axcontlem2  24593  axcontlem5  24596  axcontlem7  24598  btwnouttr  24647  btwnexch  24648  funtransport  24654  cgr3permute1  24671  colinearperm1  24685  brsegle  24731  outsideoftr  24752  outsideofeu  24754  funray  24763  funline  24765  lineunray  24770  lineelsb2  24771  ordcmp  24886  copsexgb  24966  dfoprab4pop  25037  elo  25041  splint  25048  cnvref2  25066  eloi  25086  celsor  25111  surjsec2  25120  iscst3  25176  iscst4  25177  puub2  25258  puub  25259  ismxl2  25267  ismnl2  25268  prsubrtr  25399  isidlNEW  25446  vecval1b  25451  svli2  25484  prcnt  25551  cnfilca  25556  limptlimpr2lem1  25574  issubcv  25670  ishomc  25789  ismona  25809  ismonb  25810  isepib  25820  isfunb  25835  issubcata  25846  isntr  25873  islimcat  25876  tartarmap  25888  bisig0  26062  isconcl2b  26098  isibg2  26110  bosser  26167  nn0prpwlem  26238  nn0prpw  26239  dfcon2OLD  26253  fneval  26287  topfneec  26291  filnetlem4  26330  unirep  26349  f1opr  26391  indexa  26412  sdclem1  26453  fdc  26455  neificl  26467  istotbnd  26493  sstotbnd2  26498  isbnd  26504  isbnd3b  26509  heibor1lem  26533  heiborlem3  26537  rrnheibor  26561  isrngohom  26596  isrngoiso  26609  iscrngo2  26623  isidl  26639  ispridl  26659  pridlidl  26660  pridlnr  26661  pridl  26662  ismaxidl  26665  maxidlidl  26666  smprngopr  26677  prnc  26692  brabsb2  26730  prter3  26750  ralxpxfr2d  26760  isnacs  26779  mzpclval  26803  elmzpcl  26804  mzpcompact2lem  26829  eldiophb  26836  eldioph3  26845  fz1eqin  26848  diophrex  26855  eq0rabdioph  26856  rexrabdioph  26875  dvdsrabdioph  26891  eldioph4b  26894  eldioph4i  26895  elpell1qr  26932  elpell14qr  26934  elpell1234qr  26936  pell1234qrmulcl  26940  rmydioph  27107  rmxdioph  27109  aomclem8  27159  islmodfg  27167  islssfg2  27169  islnm2  27176  frlmelbas  27224  ellspd  27254  islinds  27279  islindf4  27308  hbtlem2  27328  hbtlem5  27332  elmnc  27341  rngunsnply  27378  psgnunilem5  27417  psgnunilem3  27419  psgneldm2  27427  psgneu  27429  issdrg  27505  isdomn3  27523  expgrowth  27552  iotasbc2  27620  fvelrnbf  27689  stoweidlem31  27780  fnopafvb  28017  afvelrnb  28025  afvelrnb0  28026  mpt2xopovel  28086  usgra1v  28126  nbgrael  28141  nbgra0nb  28144  cusgra2v  28158  uvtxel  28161  trsbc  28304  e2ebind  28329  bnj206  28759  bnj1366  28862  bnj1171  29030  bnj1253  29047  bnj1417  29071  ax12-4  29106  islshp  29169  islsat  29181  islshpat  29207  lcvexchlem1  29224  lsatnem0  29235  islfl  29250  ellkr  29279  lshpsmreu  29299  lshpkrlem3  29302  cvrval2  29464  cvrnbtwn2  29465  cvrnbtwn3  29466  isat  29476  leatb  29482  leat2  29484  cvlsupr2  29533  3dim0  29646  ps-2  29667  islln  29695  islln3  29699  llnexatN  29710  islpln  29719  islpln5  29724  lplnexatN  29752  islvol  29762  islvol5  29768  dalem-cly  29860  isline  29928  ispointN  29931  ispsubsp  29934  linepsubN  29941  elpmap  29947  isline4N  29966  elpadd  29988  paddcom  30002  pmapjoin  30041  pmapjat1  30042  llnexchb2  30058  elpclN  30081  pclcmpatN  30090  ispsubclN  30126  iswatN  30183  islhp  30185  islaut  30272  ispautN  30288  isldil  30299  isltrn  30308  isltrn2N  30309  isdilN  30343  istrnN  30346  cdlemefrs29bpre0  30585  cdleme40v  30658  istendo  30949  diaelval  31223  diaeldm  31226  dibopelvalN  31333  dibopelval2  31335  dib1dim  31355  dibglbN  31356  diblsmopel  31361  dicopelval  31367  dicelvalN  31368  dicelval3  31370  dicvalrelN  31375  diclspsn  31384  dihopelvalcpre  31438  xihopellsmN  31444  dihopellsm  31445  dih1  31476  dihglblem2aN  31483  dihglblem2N  31484  dihmeetlem4preN  31496  dihglb2  31532  dvh2dim  31635  islpolN  31673  lcfl7N  31691  lcdlss  31809  hdmap1fval  31987  hdmapfval  32020  hgmapfval  32079  hdmapglem7a  32120  hdmapoc  32124
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator