MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl6bb Structured version   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  1401  19.17  1884  2eu6  2365  abeq2d  2544  necon2bbid  2656  cbvralf  2918  cbvreu  2922  cbvrab  2946  ceqsralt  2971  ralab2  3091  rexab2  3093  reu7  3121  reu8  3122  2reu5  3134  cbvralcsf  3303  cbvreucsf  3305  cbvrabcsf  3306  ralss  3401  rexss  3402  prssg  3945  ssunsn2  3950  eqsn  3952  2ralunsn  3996  eluniab  4019  elintab  4053  dfiun2g  4115  dfiin2g  4116  disjprg  4200  disjxun  4202  cbvopab1  4270  cbvmpt  4291  axsep2  4323  notzfaus  4366  opeqsn  4444  sotrieq2  4523  ordtri2  4608  oneqmini  4624  reusv3  4723  reusv6OLD  4726  reusv7OLD  4727  reuxfrd  4740  elpwunsn  4749  tfisi  4830  frsn  4940  eliunxp  5004  relop  5015  eldm2g  5058  reldm0  5079  relrn0  5120  asymref2  5243  somin1  5262  xpnz  5284  xpcan  5297  xpcan2  5298  cbviota  5415  iota1  5424  sniota  5437  fncnv  5507  fnres  5553  brprcneu  5713  fnopfvb  5760  fvelrnb  5766  funimass4  5769  dffv2  5788  fvopab3g  5794  eqfnfv  5819  eqfnfv3  5821  eqfnfv2f  5823  fvreseq  5825  fnreseql  5832  fniniseg  5843  rexsupp  5847  respreima  5851  rexrn  5864  ralrn  5865  f1ompt  5883  fsn  5898  fconstfv  5946  eufnfv  5964  rexima  5969  ralima  5970  dff13  5996  fliftfun  6026  isocnv  6042  isoini  6050  f1oiso  6063  oprabid  6097  eloprabga  6152  resoprab  6158  eqfnov  6168  eqfnov2  6169  ov6g  6203  ovelrn  6214  funimassov  6215  ovelimab  6216  ndmovg  6222  caovord2  6251  eqop  6381  releldm2  6389  dfoprab4  6396  exopxfr2  6403  bropopvvv  6418  fparlem1  6438  fparlem2  6439  xporderlem  6449  poxp  6450  soxp  6451  fnwelem  6453  mpt2xopovel  6463  brtpos2  6477  brtpos0  6478  rntpos  6484  dftpos3  6489  tpostpos  6491  tpossym  6503  tposoprab  6507  opiota  6527  cbvriota  6552  eusvobj2  6574  oevn0  6751  om00el  6811  omordlim  6812  omlimcl  6813  oeoa  6832  oeoe  6834  oeeulem  6836  oeeui  6837  oaabs2  6880  omabs  6882  erth2  6942  qliftfun  6981  erovlem  6992  ecopovsym  6998  th3qlem1  7002  elpmg  7024  elpm2g  7025  map0e  7043  dom2lem  7139  mapsnen  7176  xpdom2  7195  omxpenlem  7201  0sdomg  7228  fodomr  7250  xpf1o  7261  mapen  7263  ac6sfi  7343  marypha2lem3  7434  ordtypelem7  7485  wemaplem1  7507  wemapso2lem  7511  wemapso2  7513  elharval  7523  brwdom3  7542  unwdomg  7544  xpwdomg  7545  inf3lem1  7575  cantnfs  7613  cantnfp1lem2  7627  cantnflem1d  7636  cantnflem1  7637  mapfien  7645  wemapwe  7646  r1sdom  7692  rankr1ai  7716  rankval2  7736  unbndrank  7760  rankunb  7768  tcrank  7800  bnd2  7809  cardnueq0  7843  iscard2  7855  r0weon  7886  fseqenlem1  7897  alephord2  7949  cardaleph  7962  aceq0  7991  dfac5lem4  7999  dfac5  8001  kmlem14  8035  cfsmolem  8142  isfin4-2  8186  fin23lem26  8197  fin23lem22  8199  fin1a2lem7  8278  axdc3lem2  8323  axdc3  8326  zfac  8332  zornn0g  8377  axdclem  8391  brdom3  8398  zfcndac  8486  fpwwe2lem8  8504  fpwwe2lem12  8508  fpwwe2lem13  8509  fpwwe2  8510  pwfseqlem3  8527  winainflem  8560  eltsk2g  8618  inatsk  8645  axgroth2  8692  axgroth6  8695  sstskm  8709  ltexpi  8771  ordpinq  8812  lterpq  8839  ltanq  8840  ltmnq  8841  genpv  8868  genpelv  8869  prlem934  8902  prlem936  8916  addcmpblnr  8939  ltsrpr  8944  ltsosr  8961  mulgt0sr  8972  supsrlem  8978  elreal2  8999  ltresr  9007  ltresr2  9008  axrrecex  9030  axpre-ltadd  9034  axpre-mulgt0  9035  axpre-sup  9036  subcan2  9318  negcon1  9345  negcon2  9346  lt0neg1  9526  lt0neg2  9527  le0neg1  9528  le0neg2  9529  msq0d  9663  divmul2  9674  reclt1  9897  recgt1  9898  fimaxre  9947  infm3  9959  suprlub  9962  suprleub  9964  infmrgelb  9980  addltmul  10195  arch  10210  elznn0  10288  nn0lt10b  10328  recnz  10337  uzindOLD  10356  eluz1  10484  raluz  10517  rexuz  10519  nnwof  10535  cnref1o  10599  ltxr  10707  xrltlen  10731  dflt2  10733  xrrebnd  10748  qbtwnre  10777  xlt0neg1  10797  xlt0neg2  10798  xle0neg1  10799  xle0neg2  10800  xmulneg1  10840  supxrbnd  10899  elixx1  10917  ixxun  10924  elioo2  10949  elicc4  10969  elioopnf  10990  elioomnf  10991  iooneg  11009  iccneg  11010  iccshftr  11022  iccshftl  11024  iccdil  11026  icccntr  11028  iccf1o  11031  elfz1  11040  0fz1  11066  elfzp1  11089  fzpr  11093  fznn0  11105  uzsplit  11110  elfzm1b  11117  elfzp12  11118  fzm1  11119  injresinjlem  11191  injresinj  11192  bernneq  11497  hasheqf1o  11625  hashtpg  11683  hashbclem  11693  hashfacen  11695  hashf1  11698  2shfti  11887  sqrmsq2i  12183  limsupgle  12263  limsuple  12264  rlim  12281  clim0  12292  ello12  12302  elo12  12313  o1lo1  12323  rlimresb  12351  lo1add  12412  lo1mul  12413  rlimno1  12439  summo  12503  fsumsplit  12525  mertenslem2  12654  xpnnenOLD  12801  cnso  12838  sqr2irr  12840  dvdsval2  12847  alzdvds  12891  odd2np1lem  12899  divalgb  12916  bitsval  12928  bitsmod  12940  sadcp1  12959  gcddvds  13007  bezoutlem3  13032  bezout  13034  isprm3  13080  prmind2  13082  dvdsprime  13084  coprm  13092  prmdvdsexp  13106  crt  13159  pythagtriplem2  13183  pythagtrip  13200  pceu  13212  pc11  13245  vdwapval  13333  vdwapun  13334  vdwlem10  13350  vdwlem12  13352  vdwlem13  13353  ramval  13368  ramub1lem2  13387  prmlem0  13420  elrest  13647  imasleval  13758  ismri  13848  isacs  13868  isacs2  13870  acsfn1  13878  iscatd2  13898  homfeq  13912  catpropd  13927  ismon  13951  issect  13971  issect2  13972  isinv  13977  invsym  13979  isssc  14012  subsubc  14042  isfunc  14053  funcres2b  14086  isnat  14136  fucinv  14162  elhoma  14179  setcinv  14237  isprs  14379  isdrs  14383  istos  14456  tosso  14457  latnle  14506  isipodrs  14579  isacs5  14590  latdisd  14608  isdlat  14611  spwmo  14650  ismhm  14732  issubm  14740  grpsubeq0  14867  grpsubadd  14868  issubg  14936  subgmulg  14950  issubg3  14952  0subg  14957  isnsg  14961  eqger  14982  eqglact  14983  eqgid  14984  isghm  14998  isga  15060  gacan  15074  gaorb  15076  gastacos  15079  orbsta  15082  elcntz  15113  elcntzsn  15116  sscntz  15117  dfod2  15192  isslw  15234  sylow2alem2  15244  lsmelvalx  15266  lsmcom2  15281  lsmass  15294  lssnle  15298  pj1eu  15320  lsmhash  15329  efgi  15343  efgval2  15348  efgtlen  15350  efgred  15372  lsmcomx  15463  iscyggen2  15483  iscyg3  15488  cygabl  15492  gsumval3eu  15505  gsumzsplit  15521  eldprd  15554  subgdmdprd  15584  dprddisj2  15589  dprd2da  15592  dmdprdsplit2lem  15595  dmdprdsplit2  15596  dprdsplit  15598  dmdprdpr  15599  pgpfac1lem3  15627  pgpfac1lem4  15628  pgpfac1lem5  15629  dvdsr02  15753  isunit  15754  isirred  15796  isrhm  15816  drngunit  15832  subsubrg2  15887  issubrg3  15888  isabv  15899  islmod  15946  islss  16003  lsslss  16029  lspsnel  16071  islmhm  16095  lmhmeql  16123  islbs  16140  lsmspsn  16148  lsmelval2  16149  lspprel  16158  lvecvscan2  16176  lvecinv  16177  lspsneq  16186  lspsneu  16187  lspsolvlem  16206  islpidl  16309  lidldvgen  16318  isnzr2  16326  aspval2  16397  mplsubglem  16490  mpllsslem  16491  mplmonmul  16519  opsrtoslem2  16537  prmirredlem  16765  zrhrhmb  16784  zndvds  16822  elocv  16887  iscss  16902  pjdm  16926  ishil2  16938  isobs  16939  obslbs  16949  istop2g  16961  istopon  16982  isbasis2g  17005  isbasis3g  17006  tgss2  17044  bastop1  17050  iscld  17083  elcls  17129  ntreq0  17133  isclo  17143  isclo2  17144  islp  17196  lpdifsn  17199  islpi  17205  restsn  17226  restopn2  17233  restlp  17239  ordtbaslem  17244  ordtbas2  17247  lmbr  17314  cnprest2  17346  ist0-3  17401  ist1-2  17403  cmpsublem  17454  cmpfi  17463  1stcrest  17508  2ndcdisj  17511  1stccnp  17517  llyi  17529  nllyi  17530  lly1stc  17551  iskgen3  17573  kgencn  17580  txbas  17591  eltx  17592  elpt  17596  xkoccn  17643  ptcnplem  17645  hausdiag  17669  hauseqlcld  17670  txlm  17672  txkgen  17676  kqfvima  17754  kqt0lem  17760  r0cld  17762  regr1lem2  17764  hmeoimaf1o  17794  isfbas2  17859  fbssfi  17861  trfbas2  17867  trfil2  17911  fmfnfmlem4  17981  elflim2  17988  flimrest  18007  cnflf  18026  txflf  18030  fclsopn  18038  ufilcmp  18056  cnfcf  18066  alexsubALTlem4  18073  cnextf  18089  tmdcn2  18111  divstgpopn  18141  divstgplem  18142  eltsms  18154  tsmsgsum  18160  tsmssplit  18173  elutop  18255  ustuqtop  18268  utopsnneiplem  18269  isusp  18283  isucn  18300  iscfilu  18310  ispsmet  18327  ismet  18345  isxmet  18346  ismet2  18355  metn0  18382  elblps  18409  elbl  18410  metrest  18546  metuel2  18601  metutopOLD  18604  psmetutop  18605  restmetu  18609  dscmet  18612  nrmmetd  18614  isngp3  18637  nmogelb  18742  isnmhm  18772  qtopbaslem  18784  xrsxmet  18832  icccmplem2  18846  metdseq0  18876  elcncf  18911  cnheibor  18972  ishtpy  18989  isphtpy  18998  isphtpc  19011  om1elbas  19049  elpi1  19062  nmhmcn  19120  iscph  19125  tchcph  19186  lmmbrf  19207  iscfil  19210  iscfil2  19211  iscau  19221  caucfil  19228  iscmet  19229  iscmet3  19238  cfilucfil3OLD  19263  cfilucfil3  19264  bcthlem1  19269  minveclem3b  19321  minveclem6  19327  evthicc2  19349  ovolfioo  19356  ovolficc  19357  ovolshftlem1  19397  ovolscalem1  19401  iundisj2  19435  dyadmbl  19484  volsup2  19489  mbfmax  19533  mbfaddlem  19544  mbfsup  19548  mbfinf  19549  i1f1lem  19573  i1fres  19589  itg1climres  19598  mbfi1fseqlem4  19602  itg2leub  19618  itg2seq  19626  itg2splitlem  19632  itg2monolem1  19634  itg2mono  19637  itg2cn  19647  iblpos  19676  iblcn  19682  itgsplit  19719  ellimc2  19756  dvreslem  19788  elcpn  19812  rolle  19866  dvlip  19869  dvivth  19886  tdeglem4  19975  deg1ldg  20007  ply1nzb  20037  ply1divmo  20050  ply1divex  20051  fta1glem2  20081  plyco0  20103  elply  20106  coeeu  20136  plydivex  20206  taylthlem2  20282  radcnvlt1  20326  sincosq1sgn  20398  sincosq2sgn  20399  coseq1  20422  logreclem  20652  affineequiv  20659  dcubic  20678  quart  20693  atans2  20763  efrlim  20800  mumullem2  20955  dvdsflsumcom  20965  fsumvma2  20990  chpchtsum  20995  chpub  20996  dchrelbas  21012  dchrelbas2  21013  dchreq  21034  dchrptlem2  21041  lgsquadlem2  21131  lgsquadlem3  21132  m1lgs  21138  2sqlem6  21145  2sqlem9  21149  2sqlem10  21150  dchrisum0flb  21196  pntpbnd1  21272  pntlem3  21295  pntlemp  21296  wrdumgra  21343  usgra1v  21401  usgrafisindb1  21415  nbgraop1  21429  nbgrael  21430  nbgra0nb  21433  nbgraf1olem3  21445  nbgraf1olem5  21447  nb3graprlem2  21453  nb3grapr2  21455  cusgra2v  21463  uvtxel  21490  0wlk  21537  0trl  21538  is2wlk  21557  isspthonpth  21576  fargshiftfo  21617  usgrcyclnl1  21619  dfconngra1  21650  eupath2lem2  21692  eupath2lem3  21693  isgrpo  21776  isgrpo2  21777  isgrp2d  21815  issubgo  21883  ismgm  21900  rngosn3  22006  nvsubadd  22128  isssp  22215  islno  22246  nmogtmnf  22263  nmoubi  22265  nmounbi  22269  isblo  22275  ishmo  22304  ubthlem1  22364  ubthlem2  22365  minvecolem5  22375  minvecolem6  22376  hvmulcan2  22567  hire  22588  ocel  22775  ocsh  22777  pjhthmo  22796  shscom  22813  shmodsi  22883  elspani  23037  adjsym  23328  eigorthi  23332  nmopgtmnf  23363  adjeu  23384  adjval2  23386  cnvadj  23387  nmopub  23403  nmfnleub  23420  eleigvec  23452  nmop0h  23486  largei  23762  mdbr2  23791  mddmd2  23804  mdsl2i  23817  chrelat3  23866  atnemeq0  23872  chirredlem1  23885  sumdmdii  23910  sumdmdlem  23913  dmdbr5ati  23917  cdjreui  23927  preqsnd  23992  disjabrex  24016  disjabrexf  24017  iundisj2f  24022  ofpreima  24073  funcnv5mpt  24076  1stpreima  24087  curry2ima  24089  iundisj2fi  24145  toslub  24183  tosglb  24184  isarchi2  24247  cnvordtrestixx  24303  lmdvg  24330  ind1a  24410  braew  24585  ismbfm  24594  mbfmcnt  24610  issibf  24640  elorvc  24709  ballotlemfc0  24742  ballotlemfcc  24743  ballotlemodife  24747  subfacp1lem3  24860  subfacp1lem5  24862  subfacp1lem6  24863  erdszelem9  24877  erdszelem10  24878  erdsze2lem2  24882  iscvm  24938  cvmlift2lem10  24991  snmlval  25010  elgiso  25099  climuzcnv  25100  zmodid2  25106  mulcan2g  25182  mulsuble0b  25185  prodmo  25254  fprodsplit  25281  fprod2dlem  25296  pdivsq  25360  dfpo2  25370  br6  25372  fprb  25389  dfdm5  25392  dfrn5  25393  dfon2lem7  25408  dfon2  25411  dfrdg2  25415  predreseq  25446  wfrlem1  25530  frrlem1  25574  sltval2  25603  sltintdifex  25610  sltres  25611  nofulllem5  25653  elfuns  25752  dfiota3  25760  brimg  25774  brsuccf  25778  dfrdg4  25787  elee  25825  mptelee  25826  colinearalglem2  25838  colinearalg  25841  ax5seglem5  25864  axeuclidlem  25893  axeuclid  25894  axcontlem1  25895  axcontlem2  25896  axcontlem5  25899  axcontlem7  25901  btwnouttr  25950  btwnexch  25951  funtransport  25957  cgr3permute1  25974  colinearperm1  25988  brsegle  26034  outsideoftr  26055  outsideofeu  26057  funray  26066  funline  26068  lineunray  26073  lineelsb2  26074  ordcmp  26189  mblfinlem  26234  ismblfin  26237  mbfresfi  26243  itg2addnclem  26246  itg2addnclem2  26247  itg2addnc  26249  itg2gt0cn  26250  ftc1anclem6  26275  nn0prpwlem  26316  nn0prpw  26317  fneval  26358  topfneec  26362  filnetlem4  26401  unirep  26405  f1opr  26417  indexa  26426  sdclem1  26438  fdc  26440  neificl  26450  istotbnd  26469  sstotbnd2  26474  isbnd  26480  isbnd3b  26485  heibor1lem  26509  heiborlem3  26513  rrnheibor  26537  isrngohom  26572  isrngoiso  26585  iscrngo2  26599  isidl  26615  ispridl  26635  pridlidl  26636  pridlnr  26637  pridl  26638  ismaxidl  26641  maxidlidl  26642  smprngopr  26653  prnc  26668  brabsb2  26702  prter3  26722  ralxpxfr2d  26732  isnacs  26749  mzpclval  26773  elmzpcl  26774  mzpcompact2lem  26799  eldiophb  26806  eldioph3  26815  fz1eqin  26818  diophrex  26825  eq0rabdioph  26826  rexrabdioph  26845  dvdsrabdioph  26861  eldioph4b  26863  eldioph4i  26864  elpell1qr  26901  elpell14qr  26903  elpell1234qr  26905  pell1234qrmulcl  26909  rmydioph  27076  rmxdioph  27078  aomclem8  27127  islmodfg  27135  islssfg2  27137  islnm2  27144  frlmelbas  27192  ellspd  27222  islinds  27247  islindf4  27276  hbtlem2  27296  hbtlem5  27300  elmnc  27309  rngunsnply  27346  psgnunilem5  27385  psgnunilem3  27387  psgneldm2  27395  psgneu  27397  issdrg  27473  isdomn3  27491  expgrowth  27520  iotasbc2  27588  fvelrnbf  27656  stoweidlem31  27747  stoweidlem34  27750  stoweidlem59  27775  fnopafvb  27986  afvelrnb  27994  afvelrnb0  27995  euhash1  28145  cshwssizelem1  28243  usgra2wlkspthlem1  28259  usgra2wlkspthlem2  28260  usgra2pthlem1  28263  el2wlkonot  28289  el2spthonot  28290  2wlkonot3v  28295  2spthonot3v  28296  usg2spthonot0  28309  usg2spthonot1  28310  vdn0frgrav2  28351  vdgn0frgrav2  28352  frgrancvvdeqlem4  28359  frgrancvvdeqlem7  28362  frgrawopreglem4  28373  frg2wot1  28383  frg2woteqm  28385  2spotmdisj  28394  frgregordn0  28396  trsbc  28562  e2ebind  28587  bnj206  29035  bnj1366  29138  bnj1171  29306  bnj1253  29323  bnj1417  29347  ax7w14lemAUX7  29606  islshp  29714  islsat  29726  islshpat  29752  lcvexchlem1  29769  lsatnem0  29780  islfl  29795  ellkr  29824  lshpsmreu  29844  lshpkrlem3  29847  cvrval2  30009  cvrnbtwn2  30010  cvrnbtwn3  30011  isat  30021  leatb  30027  leat2  30029  cvlsupr2  30078  3dim0  30191  ps-2  30212  islln  30240  islln3  30244  llnexatN  30255  islpln  30264  islpln5  30269  lplnexatN  30297  islvol  30307  islvol5  30313  dalem-cly  30405  isline  30473  ispointN  30476  ispsubsp  30479  linepsubN  30486  elpmap  30492  isline4N  30511  elpadd  30533  paddcom  30547  pmapjoin  30586  pmapjat1  30587  llnexchb2  30603  elpclN  30626  pclcmpatN  30635  ispsubclN  30671  iswatN  30728  islhp  30730  islaut  30817  ispautN  30833  isldil  30844  isltrn  30853  isltrn2N  30854  isdilN  30888  istrnN  30891  cdlemefrs29bpre0  31130  cdleme40v  31203  istendo  31494  diaelval  31768  diaeldm  31771  dibopelvalN  31878  dibopelval2  31880  dib1dim  31900  dibglbN  31901  diblsmopel  31906  dicopelval  31912  dicelvalN  31913  dicelval3  31915  dicvalrelN  31920  diclspsn  31929  dihopelvalcpre  31983  xihopellsmN  31989  dihopellsm  31990  dih1  32021  dihglblem2aN  32028  dihglblem2N  32029  dihmeetlem4preN  32041  dihglb2  32077  dvh2dim  32180  islpolN  32218  lcfl7N  32236  lcdlss  32354  hdmap1fval  32532  hdmapfval  32565  hgmapfval  32624  hdmapglem7a  32665  hdmapoc  32669
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