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

Theorem syl6bb 253
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 11 . 2  |-  ( ph  ->  ( ch  <->  th )
)
41, 3bitrd 245 1  |-  ( ph  ->  ( ps  <->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  syl6rbb  254  syl6bbr  255  3bitr3g  279  bibi2i  305  ibibr  333  pm5.75  904  jaoi2  934  cadan  1398  19.17  1880  2eu6  2339  abeq2d  2513  necon2bbid  2625  cbvralf  2886  cbvreu  2890  cbvrab  2914  ceqsralt  2939  ralab2  3059  rexab2  3061  reu7  3089  reu8  3090  2reu5  3102  cbvralcsf  3271  cbvreucsf  3273  cbvrabcsf  3274  ralss  3369  rexss  3370  prssg  3913  ssunsn2  3918  eqsn  3920  2ralunsn  3964  eluniab  3987  elintab  4021  dfiun2g  4083  dfiin2g  4084  disjprg  4168  disjxun  4170  cbvopab1  4238  cbvmpt  4259  axsep2  4291  notzfaus  4334  opeqsn  4412  sotrieq2  4491  ordtri2  4576  oneqmini  4592  reusv3  4690  reusv6OLD  4693  reusv7OLD  4694  reuxfrd  4707  elpwunsn  4716  tfisi  4797  frsn  4907  eliunxp  4971  relop  4982  eldm2g  5025  reldm0  5046  relrn0  5087  asymref2  5210  somin1  5229  xpnz  5251  xpcan  5264  xpcan2  5265  cbviota  5382  iota1  5391  sniota  5404  fncnv  5474  fnres  5520  brprcneu  5680  fnopfvb  5727  fvelrnb  5733  funimass4  5736  dffv2  5755  fvopab3g  5761  eqfnfv  5786  eqfnfv3  5788  eqfnfv2f  5790  fvreseq  5792  fnreseql  5799  fniniseg  5810  rexsupp  5814  respreima  5818  rexrn  5831  ralrn  5832  f1ompt  5850  fsn  5865  fconstfv  5913  eufnfv  5931  rexima  5936  ralima  5937  dff13  5963  fliftfun  5993  isocnv  6009  isoini  6017  f1oiso  6030  oprabid  6064  eloprabga  6119  resoprab  6125  eqfnov  6135  eqfnov2  6136  ov6g  6170  ovelrn  6181  funimassov  6182  ovelimab  6183  ndmovg  6189  caovord2  6218  eqop  6348  releldm2  6356  dfoprab4  6363  exopxfr2  6370  bropopvvv  6385  fparlem1  6405  fparlem2  6406  xporderlem  6416  poxp  6417  soxp  6418  fnwelem  6420  mpt2xopovel  6430  brtpos2  6444  brtpos0  6445  rntpos  6451  dftpos3  6456  tpostpos  6458  tpossym  6470  tposoprab  6474  opiota  6494  cbvriota  6519  eusvobj2  6541  oevn0  6718  om00el  6778  omordlim  6779  omlimcl  6780  oeoa  6799  oeoe  6801  oeeulem  6803  oeeui  6804  oaabs2  6847  omabs  6849  erth2  6909  qliftfun  6948  erovlem  6959  ecopovsym  6965  th3qlem1  6969  elpmg  6991  elpm2g  6992  map0e  7010  dom2lem  7106  mapsnen  7143  xpdom2  7162  omxpenlem  7168  0sdomg  7195  fodomr  7217  xpf1o  7228  mapen  7230  ac6sfi  7310  marypha2lem3  7400  ordtypelem7  7449  wemaplem1  7471  wemapso2lem  7475  wemapso2  7477  elharval  7487  brwdom3  7506  unwdomg  7508  xpwdomg  7509  inf3lem1  7539  cantnfs  7577  cantnfp1lem2  7591  cantnflem1d  7600  cantnflem1  7601  mapfien  7609  wemapwe  7610  r1sdom  7656  rankr1ai  7680  rankval2  7700  unbndrank  7724  rankunb  7732  tcrank  7764  bnd2  7773  cardnueq0  7807  iscard2  7819  r0weon  7850  fseqenlem1  7861  alephord2  7913  cardaleph  7926  aceq0  7955  dfac5lem4  7963  dfac5  7965  kmlem14  7999  cfsmolem  8106  isfin4-2  8150  fin23lem26  8161  fin23lem22  8163  fin1a2lem7  8242  axdc3lem2  8287  axdc3  8290  zfac  8296  zornn0g  8341  axdclem  8355  brdom3  8362  zfcndac  8450  fpwwe2lem8  8468  fpwwe2lem12  8472  fpwwe2lem13  8473  fpwwe2  8474  pwfseqlem3  8491  winainflem  8524  eltsk2g  8582  inatsk  8609  axgroth2  8656  axgroth6  8659  sstskm  8673  ltexpi  8735  ordpinq  8776  lterpq  8803  ltanq  8804  ltmnq  8805  genpv  8832  genpelv  8833  prlem934  8866  prlem936  8880  addcmpblnr  8903  ltsrpr  8908  ltsosr  8925  mulgt0sr  8936  supsrlem  8942  elreal2  8963  ltresr  8971  ltresr2  8972  axrrecex  8994  axpre-ltadd  8998  axpre-mulgt0  8999  axpre-sup  9000  subcan2  9282  negcon1  9309  negcon2  9310  lt0neg1  9490  lt0neg2  9491  le0neg1  9492  le0neg2  9493  msq0d  9627  divmul2  9638  reclt1  9861  recgt1  9862  fimaxre  9911  infm3  9923  suprlub  9926  suprleub  9928  infmrgelb  9944  addltmul  10159  arch  10174  elznn0  10252  nn0lt10b  10292  recnz  10301  uzindOLD  10320  eluz1  10448  raluz  10481  rexuz  10483  nnwof  10499  cnref1o  10563  ltxr  10671  xrltlen  10695  dflt2  10697  xrrebnd  10712  qbtwnre  10741  xlt0neg1  10761  xlt0neg2  10762  xle0neg1  10763  xle0neg2  10764  xmulneg1  10804  supxrbnd  10863  elixx1  10881  ixxun  10888  elioo2  10913  elicc4  10933  elioopnf  10954  elioomnf  10955  iooneg  10973  iccneg  10974  iccshftr  10986  iccshftl  10988  iccdil  10990  icccntr  10992  iccf1o  10995  elfz1  11004  0fz1  11030  elfzp1  11053  fzpr  11057  fznn0  11069  uzsplit  11073  elfzm1b  11080  elfzp12  11081  fzm1  11082  injresinjlem  11154  injresinj  11155  bernneq  11460  hasheqf1o  11588  hashtpg  11646  hashbclem  11656  hashfacen  11658  hashf1  11661  2shfti  11850  sqrmsq2i  12146  limsupgle  12226  limsuple  12227  rlim  12244  clim0  12255  ello12  12265  elo12  12276  o1lo1  12286  rlimresb  12314  lo1add  12375  lo1mul  12376  rlimno1  12402  summo  12466  fsumsplit  12488  mertenslem2  12617  xpnnenOLD  12764  cnso  12801  sqr2irr  12803  dvdsval2  12810  alzdvds  12854  odd2np1lem  12862  divalgb  12879  bitsval  12891  bitsmod  12903  sadcp1  12922  gcddvds  12970  bezoutlem3  12995  bezout  12997  isprm3  13043  prmind2  13045  dvdsprime  13047  coprm  13055  prmdvdsexp  13069  crt  13122  pythagtriplem2  13146  pythagtrip  13163  pceu  13175  pc11  13208  vdwapval  13296  vdwapun  13297  vdwlem10  13313  vdwlem12  13315  vdwlem13  13316  ramval  13331  ramub1lem2  13350  prmlem0  13383  elrest  13610  imasleval  13721  ismri  13811  isacs  13831  isacs2  13833  acsfn1  13841  iscatd2  13861  homfeq  13875  catpropd  13890  ismon  13914  issect  13934  issect2  13935  isinv  13940  invsym  13942  isssc  13975  subsubc  14005  isfunc  14016  funcres2b  14049  isnat  14099  fucinv  14125  elhoma  14142  setcinv  14200  isprs  14342  isdrs  14346  istos  14419  tosso  14420  latnle  14469  isipodrs  14542  isacs5  14553  latdisd  14571  isdlat  14574  spwmo  14613  ismhm  14695  issubm  14703  grpsubeq0  14830  grpsubadd  14831  issubg  14899  subgmulg  14913  issubg3  14915  0subg  14920  isnsg  14924  eqger  14945  eqglact  14946  eqgid  14947  isghm  14961  isga  15023  gacan  15037  gaorb  15039  gastacos  15042  orbsta  15045  elcntz  15076  elcntzsn  15079  sscntz  15080  dfod2  15155  isslw  15197  sylow2alem2  15207  lsmelvalx  15229  lsmcom2  15244  lsmass  15257  lssnle  15261  pj1eu  15283  lsmhash  15292  efgi  15306  efgval2  15311  efgtlen  15313  efgred  15335  lsmcomx  15426  iscyggen2  15446  iscyg3  15451  cygabl  15455  gsumval3eu  15468  gsumzsplit  15484  eldprd  15517  subgdmdprd  15547  dprddisj2  15552  dprd2da  15555  dmdprdsplit2lem  15558  dmdprdsplit2  15559  dprdsplit  15561  dmdprdpr  15562  pgpfac1lem3  15590  pgpfac1lem4  15591  pgpfac1lem5  15592  dvdsr02  15716  isunit  15717  isirred  15759  isrhm  15779  drngunit  15795  subsubrg2  15850  issubrg3  15851  isabv  15862  islmod  15909  islss  15966  lsslss  15992  lspsnel  16034  islmhm  16058  lmhmeql  16086  islbs  16103  lsmspsn  16111  lsmelval2  16112  lspprel  16121  lvecvscan2  16139  lvecinv  16140  lspsneq  16149  lspsneu  16150  lspsolvlem  16169  islpidl  16272  lidldvgen  16281  isnzr2  16289  aspval2  16360  mplsubglem  16453  mpllsslem  16454  mplmonmul  16482  opsrtoslem2  16500  prmirredlem  16728  zrhrhmb  16747  zndvds  16785  elocv  16850  iscss  16865  pjdm  16889  ishil2  16901  isobs  16902  obslbs  16912  istop2g  16924  istopon  16945  isbasis2g  16968  isbasis3g  16969  tgss2  17007  bastop1  17013  iscld  17046  elcls  17092  ntreq0  17096  isclo  17106  isclo2  17107  islp  17159  lpdifsn  17162  islpi  17167  restsn  17188  restopn2  17195  restlp  17201  ordtbaslem  17206  ordtbas2  17209  lmbr  17276  cnprest2  17308  ist0-3  17363  ist1-2  17365  cmpsublem  17416  cmpfi  17425  1stcrest  17469  2ndcdisj  17472  1stccnp  17478  llyi  17490  nllyi  17491  lly1stc  17512  iskgen3  17534  kgencn  17541  txbas  17552  eltx  17553  elpt  17557  xkoccn  17604  ptcnplem  17606  hausdiag  17630  hauseqlcld  17631  txlm  17633  txkgen  17637  kqfvima  17715  kqt0lem  17721  r0cld  17723  regr1lem2  17725  hmeoimaf1o  17755  isfbas2  17820  fbssfi  17822  trfbas2  17828  trfil2  17872  fmfnfmlem4  17942  elflim2  17949  flimrest  17968  cnflf  17987  txflf  17991  fclsopn  17999  ufilcmp  18017  cnfcf  18027  alexsubALTlem4  18034  cnextf  18050  tmdcn2  18072  divstgpopn  18102  divstgplem  18103  eltsms  18115  tsmsgsum  18121  tsmssplit  18134  elutop  18216  ustuqtop  18229  utopsnneiplem  18230  isusp  18244  isucn  18261  iscfilu  18271  ispsmet  18288  ismet  18306  isxmet  18307  ismet2  18316  metn0  18343  elblps  18370  elbl  18371  metrest  18507  metuel2  18562  metutopOLD  18565  psmetutop  18566  restmetu  18570  dscmet  18573  nrmmetd  18575  isngp3  18598  nmogelb  18703  isnmhm  18733  qtopbaslem  18745  xrsxmet  18793  icccmplem2  18807  metdseq0  18837  elcncf  18872  cnheibor  18933  ishtpy  18950  isphtpy  18959  isphtpc  18972  om1elbas  19010  elpi1  19023  nmhmcn  19081  iscph  19086  tchcph  19147  lmmbrf  19168  iscfil  19171  iscfil2  19172  iscau  19182  caucfil  19189  iscmet  19190  iscmet3  19199  cfilucfil3OLD  19224  cfilucfil3  19225  bcthlem1  19230  minveclem3b  19282  minveclem6  19288  evthicc2  19310  ovolfioo  19317  ovolficc  19318  ovolshftlem1  19358  ovolscalem1  19362  iundisj2  19396  dyadmbl  19445  volsup2  19450  mbfmax  19494  mbfaddlem  19505  mbfsup  19509  mbfinf  19510  i1f1lem  19534  i1fres  19550  itg1climres  19559  mbfi1fseqlem4  19563  itg2leub  19579  itg2seq  19587  itg2splitlem  19593  itg2monolem1  19595  itg2mono  19598  itg2cn  19608  iblpos  19637  iblcn  19643  itgsplit  19680  ellimc2  19717  dvreslem  19749  elcpn  19773  rolle  19827  dvlip  19830  dvivth  19847  tdeglem4  19936  deg1ldg  19968  ply1nzb  19998  ply1divmo  20011  ply1divex  20012  fta1glem2  20042  plyco0  20064  elply  20067  coeeu  20097  plydivex  20167  taylthlem2  20243  radcnvlt1  20287  sincosq1sgn  20359  sincosq2sgn  20360  coseq1  20383  logreclem  20613  affineequiv  20620  dcubic  20639  quart  20654  atans2  20724  efrlim  20761  mumullem2  20916  dvdsflsumcom  20926  fsumvma2  20951  chpchtsum  20956  chpub  20957  dchrelbas  20973  dchrelbas2  20974  dchreq  20995  dchrptlem2  21002  lgsquadlem2  21092  lgsquadlem3  21093  m1lgs  21099  2sqlem6  21106  2sqlem9  21110  2sqlem10  21111  dchrisum0flb  21157  pntpbnd1  21233  pntlem3  21256  pntlemp  21257  wrdumgra  21304  usgra1v  21362  usgrafisindb1  21376  nbgraop1  21390  nbgrael  21391  nbgra0nb  21394  nbgraf1olem3  21406  nbgraf1olem5  21408  nb3graprlem2  21414  nb3grapr2  21416  cusgra2v  21424  uvtxel  21451  0wlk  21498  0trl  21499  is2wlk  21518  isspthonpth  21537  fargshiftfo  21578  usgrcyclnl1  21580  dfconngra1  21611  eupath2lem2  21653  eupath2lem3  21654  isgrpo  21737  isgrpo2  21738  isgrp2d  21776  issubgo  21844  ismgm  21861  rngosn3  21967  nvsubadd  22089  isssp  22176  islno  22207  nmogtmnf  22224  nmoubi  22226  nmounbi  22230  isblo  22236  ishmo  22265  ubthlem1  22325  ubthlem2  22326  minvecolem5  22336  minvecolem6  22337  hvmulcan2  22528  hire  22549  ocel  22736  ocsh  22738  pjhthmo  22757  shscom  22774  shmodsi  22844  elspani  22998  adjsym  23289  eigorthi  23293  nmopgtmnf  23324  adjeu  23345  adjval2  23347  cnvadj  23348  nmopub  23364  nmfnleub  23381  eleigvec  23413  nmop0h  23447  largei  23723  mdbr2  23752  mddmd2  23765  mdsl2i  23778  chrelat3  23827  atnemeq0  23833  chirredlem1  23846  sumdmdii  23871  sumdmdlem  23874  dmdbr5ati  23878  cdjreui  23888  preqsnd  23953  disjabrex  23977  disjabrexf  23978  iundisj2f  23983  ofpreima  24034  funcnv5mpt  24037  1stpreima  24048  curry2ima  24050  iundisj2fi  24106  toslub  24144  tosglb  24145  isarchi2  24208  cnvordtrestixx  24264  lmdvg  24291  ind1a  24371  braew  24546  ismbfm  24555  mbfmcnt  24571  issibf  24601  elorvc  24670  ballotlemfc0  24703  ballotlemfcc  24704  ballotlemodife  24708  subfacp1lem3  24821  subfacp1lem5  24823  subfacp1lem6  24824  erdszelem9  24838  erdszelem10  24839  erdsze2lem2  24843  iscvm  24899  cvmlift2lem10  24952  snmlval  24971  elgiso  25060  climuzcnv  25061  zmodid2  25067  mulcan2g  25143  mulsuble0b  25146  prodmo  25215  fprodsplit  25242  fprod2dlem  25257  pdivsq  25316  dfpo2  25326  br6  25328  fprb  25343  dfdm5  25346  dfrn5  25347  dfon2lem7  25359  dfon2  25362  dfrdg2  25366  predreseq  25393  wfrlem1  25470  frrlem1  25495  sltval2  25524  sltintdifex  25531  sltres  25532  nofulllem5  25574  dfiota3  25676  brimg  25690  brsuccf  25694  dfrdg4  25703  elee  25737  mptelee  25738  colinearalglem2  25750  colinearalg  25753  ax5seglem5  25776  axeuclidlem  25805  axeuclid  25806  axcontlem1  25807  axcontlem2  25808  axcontlem5  25811  axcontlem7  25813  btwnouttr  25862  btwnexch  25863  funtransport  25869  cgr3permute1  25886  colinearperm1  25900  brsegle  25946  outsideoftr  25967  outsideofeu  25969  funray  25978  funline  25980  lineunray  25985  lineelsb2  25986  ordcmp  26101  mblfinlem  26143  ismblfin  26146  mbfresfi  26152  itg2addnclem  26155  itg2addnclem2  26156  itg2addnc  26158  itg2gt0cn  26159  nn0prpwlem  26215  nn0prpw  26216  fneval  26257  topfneec  26261  filnetlem4  26300  unirep  26304  f1opr  26316  indexa  26325  sdclem1  26337  fdc  26339  neificl  26349  istotbnd  26368  sstotbnd2  26373  isbnd  26379  isbnd3b  26384  heibor1lem  26408  heiborlem3  26412  rrnheibor  26436  isrngohom  26471  isrngoiso  26484  iscrngo2  26498  isidl  26514  ispridl  26534  pridlidl  26535  pridlnr  26536  pridl  26537  ismaxidl  26540  maxidlidl  26541  smprngopr  26552  prnc  26567  brabsb2  26601  prter3  26621  ralxpxfr2d  26631  isnacs  26648  mzpclval  26672  elmzpcl  26673  mzpcompact2lem  26698  eldiophb  26705  eldioph3  26714  fz1eqin  26717  diophrex  26724  eq0rabdioph  26725  rexrabdioph  26744  dvdsrabdioph  26760  eldioph4b  26762  eldioph4i  26763  elpell1qr  26800  elpell14qr  26802  elpell1234qr  26804  pell1234qrmulcl  26808  rmydioph  26975  rmxdioph  26977  aomclem8  27027  islmodfg  27035  islssfg2  27037  islnm2  27044  frlmelbas  27092  ellspd  27122  islinds  27147  islindf4  27176  hbtlem2  27196  hbtlem5  27200  elmnc  27209  rngunsnply  27246  psgnunilem5  27285  psgnunilem3  27287  psgneldm2  27295  psgneu  27297  issdrg  27373  isdomn3  27391  expgrowth  27420  iotasbc2  27488  fvelrnbf  27556  stoweidlem31  27647  stoweidlem34  27650  stoweidlem59  27675  fnopafvb  27886  afvelrnb  27894  afvelrnb0  27895  euhash1  27998  usgra2wlkspthlem1  28036  usgra2wlkspthlem2  28037  usgra2pthlem1  28040  el2wlkonot  28066  el2spthonot  28067  2wlkonot3v  28072  2spthonot3v  28073  usg2spthonot0  28086  usg2spthonot1  28087  vdn0frgrav2  28128  vdgn0frgrav2  28129  frgrancvvdeqlem4  28136  frgrancvvdeqlem7  28139  frgrawopreglem4  28150  frg2wot1  28160  frg2woteqm  28162  2spotmdisj  28171  frgregordn0  28173  trsbc  28336  e2ebind  28361  bnj206  28804  bnj1366  28907  bnj1171  29075  bnj1253  29092  bnj1417  29116  islshp  29462  islsat  29474  islshpat  29500  lcvexchlem1  29517  lsatnem0  29528  islfl  29543  ellkr  29572  lshpsmreu  29592  lshpkrlem3  29595  cvrval2  29757  cvrnbtwn2  29758  cvrnbtwn3  29759  isat  29769  leatb  29775  leat2  29777  cvlsupr2  29826  3dim0  29939  ps-2  29960  islln  29988  islln3  29992  llnexatN  30003  islpln  30012  islpln5  30017  lplnexatN  30045  islvol  30055  islvol5  30061  dalem-cly  30153  isline  30221  ispointN  30224  ispsubsp  30227  linepsubN  30234  elpmap  30240  isline4N  30259  elpadd  30281  paddcom  30295  pmapjoin  30334  pmapjat1  30335  llnexchb2  30351  elpclN  30374  pclcmpatN  30383  ispsubclN  30419  iswatN  30476  islhp  30478  islaut  30565  ispautN  30581  isldil  30592  isltrn  30601  isltrn2N  30602  isdilN  30636  istrnN  30639  cdlemefrs29bpre0  30878  cdleme40v  30951  istendo  31242  diaelval  31516  diaeldm  31519  dibopelvalN  31626  dibopelval2  31628  dib1dim  31648  dibglbN  31649  diblsmopel  31654  dicopelval  31660  dicelvalN  31661  dicelval3  31663  dicvalrelN  31668  diclspsn  31677  dihopelvalcpre  31731  xihopellsmN  31737  dihopellsm  31738  dih1  31769  dihglblem2aN  31776  dihglblem2N  31777  dihmeetlem4preN  31789  dihglb2  31825  dvh2dim  31928  islpolN  31966  lcfl7N  31984  lcdlss  32102  hdmap1fval  32280  hdmapfval  32313  hgmapfval  32372  hdmapglem7a  32413  hdmapoc  32417
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 178
  Copyright terms: Public domain W3C validator