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  1873  2eu6  2324  abeq2d  2497  necon2bbid  2609  cbvralf  2870  cbvreu  2874  cbvrab  2898  ceqsralt  2923  ralab2  3043  rexab2  3045  reu7  3073  reu8  3074  2reu5  3086  cbvralcsf  3255  cbvreucsf  3257  cbvrabcsf  3258  ralss  3353  rexss  3354  prssg  3897  ssunsn2  3902  eqsn  3904  2ralunsn  3947  eluniab  3970  elintab  4004  dfiun2g  4066  dfiin2g  4067  disjprg  4150  disjxun  4152  cbvopab1  4220  cbvmpt  4241  axsep2  4273  notzfaus  4316  opeqsn  4394  sotrieq2  4473  ordtri2  4558  oneqmini  4574  reusv3  4672  reusv6OLD  4675  reusv7OLD  4676  reuxfrd  4689  elpwunsn  4698  tfisi  4779  frsn  4889  eliunxp  4953  relop  4964  eldm2g  5007  reldm0  5028  relrn0  5069  asymref2  5192  somin1  5211  xpnz  5233  xpcan  5246  xpcan2  5247  cbviota  5364  iota1  5373  sniota  5386  fncnv  5456  fnres  5502  brprcneu  5662  fnopfvb  5708  fvelrnb  5714  funimass4  5717  dffv2  5736  fvopab3g  5742  eqfnfv  5767  eqfnfv3  5769  eqfnfv2f  5771  fvreseq  5773  fnreseql  5780  fniniseg  5791  rexsupp  5795  respreima  5799  rexrn  5812  ralrn  5813  f1ompt  5831  fsn  5846  fconstfv  5894  eufnfv  5912  rexima  5917  ralima  5918  dff13  5944  fliftfun  5974  isocnv  5990  isoini  5998  f1oiso  6011  oprabid  6045  eloprabga  6100  resoprab  6106  eqfnov  6116  eqfnov2  6117  ov6g  6151  ovelrn  6162  funimassov  6163  ovelimab  6164  ndmovg  6170  caovord2  6199  eqop  6329  releldm2  6337  dfoprab4  6344  exopxfr2  6351  bropopvvv  6366  fparlem1  6386  fparlem2  6387  xporderlem  6394  poxp  6395  soxp  6396  fnwelem  6398  mpt2xopovel  6408  brtpos2  6422  brtpos0  6423  rntpos  6429  dftpos3  6434  tpostpos  6436  tpossym  6448  tposoprab  6452  opiota  6472  cbvriota  6497  eusvobj2  6519  oevn0  6696  om00el  6756  omordlim  6757  omlimcl  6758  oeoa  6777  oeoe  6779  oeeulem  6781  oeeui  6782  oaabs2  6825  omabs  6827  erth2  6887  qliftfun  6926  erovlem  6937  ecopovsym  6943  th3qlem1  6947  elpmg  6969  elpm2g  6970  map0e  6988  dom2lem  7084  mapsnen  7121  xpdom2  7140  omxpenlem  7146  0sdomg  7173  fodomr  7195  xpf1o  7206  mapen  7208  ac6sfi  7288  marypha2lem3  7378  ordtypelem7  7427  wemaplem1  7449  wemapso2lem  7453  wemapso2  7455  elharval  7465  brwdom3  7484  unwdomg  7486  xpwdomg  7487  inf3lem1  7517  cantnfs  7555  cantnfp1lem2  7569  cantnflem1d  7578  cantnflem1  7579  mapfien  7587  wemapwe  7588  r1sdom  7634  rankr1ai  7658  rankval2  7678  unbndrank  7702  rankunb  7710  tcrank  7742  bnd2  7751  cardnueq0  7785  iscard2  7797  r0weon  7828  fseqenlem1  7839  alephord2  7891  cardaleph  7904  aceq0  7933  dfac5lem4  7941  dfac5  7943  kmlem14  7977  cfsmolem  8084  isfin4-2  8128  fin23lem26  8139  fin23lem22  8141  fin1a2lem7  8220  axdc3lem2  8265  axdc3  8268  zfac  8274  zornn0g  8319  axdclem  8333  brdom3  8340  zfcndac  8428  fpwwe2lem8  8446  fpwwe2lem12  8450  fpwwe2lem13  8451  fpwwe2  8452  pwfseqlem3  8469  winainflem  8502  eltsk2g  8560  inatsk  8587  axgroth2  8634  axgroth6  8637  sstskm  8651  ltexpi  8713  ordpinq  8754  lterpq  8781  ltanq  8782  ltmnq  8783  genpv  8810  genpelv  8811  prlem934  8844  prlem936  8858  addcmpblnr  8881  ltsrpr  8886  ltsosr  8903  mulgt0sr  8914  supsrlem  8920  elreal2  8941  ltresr  8949  ltresr2  8950  axrrecex  8972  axpre-ltadd  8976  axpre-mulgt0  8977  axpre-sup  8978  subcan2  9259  negcon1  9286  negcon2  9287  lt0neg1  9467  lt0neg2  9468  le0neg1  9469  le0neg2  9470  msq0d  9604  divmul2  9615  reclt1  9838  recgt1  9839  fimaxre  9888  infm3  9900  suprlub  9903  suprleub  9905  infmrgelb  9921  addltmul  10136  arch  10151  elznn0  10229  nn0lt10b  10269  recnz  10278  uzindOLD  10297  eluz1  10425  raluz  10458  rexuz  10460  nnwof  10476  cnref1o  10540  ltxr  10648  xrltlen  10672  dflt2  10674  xrrebnd  10689  qbtwnre  10718  xlt0neg1  10738  xlt0neg2  10739  xle0neg1  10740  xle0neg2  10741  xmulneg1  10781  supxrbnd  10840  elixx1  10858  ixxun  10865  elioo2  10890  elicc4  10910  elioopnf  10931  elioomnf  10932  iooneg  10950  iccneg  10951  iccshftr  10963  iccshftl  10965  iccdil  10967  icccntr  10969  iccf1o  10972  elfz1  10981  0fz1  11007  elfzp1  11030  fzpr  11034  fznn0  11045  uzsplit  11049  elfzm1b  11056  elfzp12  11057  fzm1  11058  injresinjlem  11127  injresinj  11128  bernneq  11433  hasheqf1o  11561  hashtpg  11619  hashbclem  11629  hashfacen  11631  hashf1  11634  2shfti  11823  sqrmsq2i  12119  limsupgle  12199  limsuple  12200  rlim  12217  clim0  12228  ello12  12238  elo12  12249  o1lo1  12259  rlimresb  12287  lo1add  12348  lo1mul  12349  rlimno1  12375  summo  12439  fsumsplit  12461  mertenslem2  12590  xpnnenOLD  12737  cnso  12774  sqr2irr  12776  dvdsval2  12783  alzdvds  12827  odd2np1lem  12835  divalgb  12852  bitsval  12864  bitsmod  12876  sadcp1  12895  gcddvds  12943  bezoutlem3  12968  bezout  12970  isprm3  13016  prmind2  13018  dvdsprime  13020  coprm  13028  prmdvdsexp  13042  crt  13095  pythagtriplem2  13119  pythagtrip  13136  pceu  13148  pc11  13181  vdwapval  13269  vdwapun  13270  vdwlem10  13286  vdwlem12  13288  vdwlem13  13289  ramval  13304  ramub1lem2  13323  prmlem0  13356  elrest  13583  imasleval  13694  ismri  13784  isacs  13804  isacs2  13806  acsfn1  13814  iscatd2  13834  homfeq  13848  catpropd  13863  ismon  13887  issect  13907  issect2  13908  isinv  13913  invsym  13915  isssc  13948  subsubc  13978  isfunc  13989  funcres2b  14022  isnat  14072  fucinv  14098  elhoma  14115  setcinv  14173  isprs  14315  isdrs  14319  istos  14392  tosso  14393  latnle  14442  isipodrs  14515  isacs5  14526  latdisd  14544  isdlat  14547  spwmo  14586  ismhm  14668  issubm  14676  grpsubeq0  14803  grpsubadd  14804  issubg  14872  subgmulg  14886  issubg3  14888  0subg  14893  isnsg  14897  eqger  14918  eqglact  14919  eqgid  14920  isghm  14934  isga  14996  gacan  15010  gaorb  15012  gastacos  15015  orbsta  15018  elcntz  15049  elcntzsn  15052  sscntz  15053  dfod2  15128  isslw  15170  sylow2alem2  15180  lsmelvalx  15202  lsmcom2  15217  lsmass  15230  lssnle  15234  pj1eu  15256  lsmhash  15265  efgi  15279  efgval2  15284  efgtlen  15286  efgred  15308  lsmcomx  15399  iscyggen2  15419  iscyg3  15424  cygabl  15428  gsumval3eu  15441  gsumzsplit  15457  eldprd  15490  subgdmdprd  15520  dprddisj2  15525  dprd2da  15528  dmdprdsplit2lem  15531  dmdprdsplit2  15532  dprdsplit  15534  dmdprdpr  15535  pgpfac1lem3  15563  pgpfac1lem4  15564  pgpfac1lem5  15565  dvdsr02  15689  isunit  15690  isirred  15732  isrhm  15752  drngunit  15768  subsubrg2  15823  issubrg3  15824  isabv  15835  islmod  15882  islss  15939  lsslss  15965  lspsnel  16007  islmhm  16031  lmhmeql  16059  islbs  16076  lsmspsn  16084  lsmelval2  16085  lspprel  16094  lvecvscan2  16112  lvecinv  16113  lspsneq  16122  lspsneu  16123  lspsolvlem  16142  islpidl  16245  lidldvgen  16254  isnzr2  16262  aspval2  16333  mplsubglem  16426  mpllsslem  16427  mplmonmul  16455  opsrtoslem2  16473  prmirredlem  16697  zrhrhmb  16716  zndvds  16754  elocv  16819  iscss  16834  pjdm  16858  ishil2  16870  isobs  16871  obslbs  16881  istop2g  16893  istopon  16914  isbasis2g  16937  isbasis3g  16938  tgss2  16976  bastop1  16982  iscld  17015  elcls  17061  ntreq0  17065  isclo  17075  isclo2  17076  islp  17128  lpdifsn  17131  islpi  17136  restsn  17157  restopn2  17164  restlp  17170  ordtbaslem  17175  ordtbas2  17178  lmbr  17245  cnprest2  17277  ist0-3  17332  ist1-2  17334  cmpsublem  17385  cmpfi  17394  1stcrest  17438  2ndcdisj  17441  1stccnp  17447  llyi  17459  nllyi  17460  lly1stc  17481  iskgen3  17503  kgencn  17510  txbas  17521  eltx  17522  elpt  17526  xkoccn  17573  ptcnplem  17575  hausdiag  17599  hauseqlcld  17600  txlm  17602  txkgen  17606  kqfvima  17684  kqt0lem  17690  r0cld  17692  regr1lem2  17694  hmeoimaf1o  17724  isfbas2  17789  fbssfi  17791  trfbas2  17797  trfil2  17841  fmfnfmlem4  17911  elflim2  17918  flimrest  17937  cnflf  17956  txflf  17960  fclsopn  17968  ufilcmp  17986  cnfcf  17996  alexsubALTlem4  18003  cnextf  18019  tmdcn2  18041  divstgpopn  18071  divstgplem  18072  eltsms  18084  tsmsgsum  18090  tsmssplit  18103  elutop  18185  ustuqtop  18198  utopsnneiplem  18199  isusp  18213  isucn  18230  iscfilu  18240  ismet  18263  isxmet  18264  ismet2  18273  metn0  18299  elbl  18324  metrest  18445  metuel2  18486  metutop  18488  restmetu  18490  dscmet  18492  nrmmetd  18494  isngp3  18517  nmogelb  18622  isnmhm  18652  qtopbaslem  18664  xrsxmet  18712  icccmplem2  18726  metdseq0  18756  elcncf  18791  cnheibor  18852  ishtpy  18869  isphtpy  18878  isphtpc  18891  om1elbas  18929  elpi1  18942  nmhmcn  19000  iscph  19005  tchcph  19066  lmmbrf  19087  iscfil  19090  iscfil2  19091  iscau  19101  caucfil  19108  iscmet  19109  iscmet3  19118  cfilucfil3  19143  bcthlem1  19147  minveclem3b  19197  minveclem6  19203  evthicc2  19225  ovolfioo  19232  ovolficc  19233  ovolshftlem1  19273  ovolscalem1  19277  iundisj2  19311  dyadmbl  19360  volsup2  19365  mbfmax  19409  mbfaddlem  19420  mbfsup  19424  mbfinf  19425  i1f1lem  19449  i1fres  19465  itg1climres  19474  mbfi1fseqlem4  19478  itg2leub  19494  itg2seq  19502  itg2splitlem  19508  itg2monolem1  19510  itg2mono  19513  itg2cn  19523  iblpos  19552  iblcn  19558  itgsplit  19595  ellimc2  19632  dvreslem  19664  elcpn  19688  rolle  19742  dvlip  19745  dvivth  19762  tdeglem4  19851  deg1ldg  19883  ply1nzb  19913  ply1divmo  19926  ply1divex  19927  fta1glem2  19957  plyco0  19979  elply  19982  coeeu  20012  plydivex  20082  taylthlem2  20158  radcnvlt1  20202  sincosq1sgn  20274  sincosq2sgn  20275  coseq1  20298  logreclem  20528  affineequiv  20535  dcubic  20554  quart  20569  atans2  20639  efrlim  20676  mumullem2  20831  dvdsflsumcom  20841  fsumvma2  20866  chpchtsum  20871  chpub  20872  dchrelbas  20888  dchrelbas2  20889  dchreq  20910  dchrptlem2  20917  lgsquadlem2  21007  lgsquadlem3  21008  m1lgs  21014  2sqlem6  21021  2sqlem9  21025  2sqlem10  21026  dchrisum0flb  21072  pntpbnd1  21148  pntlem3  21171  pntlemp  21172  wrdumgra  21219  usgra1v  21276  usgrafisindb1  21290  nbgraop1  21304  nbgrael  21305  nbgra0nb  21308  nbgraf1olem3  21320  nbgraf1olem5  21322  nb3graprlem2  21328  nb3grapr2  21330  cusgra2v  21338  uvtxel  21365  0wlk  21410  0trl  21411  fargshiftfo  21474  usgrcyclnl1  21476  dfconngra1  21507  eupath2lem2  21549  eupath2lem3  21550  isgrpo  21633  isgrpo2  21634  isgrp2d  21672  issubgo  21740  ismgm  21757  rngosn3  21863  nvsubadd  21985  isssp  22072  islno  22103  nmogtmnf  22120  nmoubi  22122  nmounbi  22126  isblo  22132  ishmo  22161  ubthlem1  22221  ubthlem2  22222  minvecolem5  22232  minvecolem6  22233  hvmulcan2  22424  hire  22445  ocel  22632  ocsh  22634  pjhthmo  22653  shscom  22670  shmodsi  22740  elspani  22894  adjsym  23185  eigorthi  23189  nmopgtmnf  23220  adjeu  23241  adjval2  23243  cnvadj  23244  nmopub  23260  nmfnleub  23277  eleigvec  23309  nmop0h  23343  largei  23619  mdbr2  23648  mddmd2  23661  mdsl2i  23674  chrelat3  23723  atnemeq0  23729  chirredlem1  23742  sumdmdii  23767  sumdmdlem  23770  dmdbr5ati  23774  cdjreui  23784  preqsnd  23845  disjabrex  23869  disjabrexf  23870  iundisj2f  23874  funcnv5mpt  23926  1stpreima  23937  curry2ima  23939  iundisj2fi  23992  cnvordtrestixx  24116  lmdvg  24143  ind1a  24215  braew  24388  ismbfm  24397  mbfmcnt  24413  elorvc  24497  ballotlemfc0  24530  ballotlemfcc  24531  ballotlemodife  24535  subfacp1lem3  24648  subfacp1lem5  24650  subfacp1lem6  24651  erdszelem9  24665  erdszelem10  24666  erdsze2lem2  24670  iscvm  24726  cvmlift2lem10  24779  snmlval  24798  elgiso  24887  climuzcnv  24888  zmodid2  24894  mulcan2g  24970  mulsuble0b  24973  prodmo  25042  fprodsplit  25069  pdivsq  25127  dfpo2  25137  br6  25139  fprb  25154  dfdm5  25157  dfrn5  25158  dfon2lem7  25170  dfon2  25173  dfrdg2  25177  predreseq  25204  wfrlem1  25281  frrlem1  25306  sltval2  25335  sltintdifex  25342  sltres  25343  nofulllem5  25385  dfiota3  25487  brimg  25501  brsuccf  25505  dfrdg4  25514  elee  25548  mptelee  25549  colinearalglem2  25561  colinearalg  25564  ax5seglem5  25587  axeuclidlem  25616  axeuclid  25617  axcontlem1  25618  axcontlem2  25619  axcontlem5  25622  axcontlem7  25624  btwnouttr  25673  btwnexch  25674  funtransport  25680  cgr3permute1  25697  colinearperm1  25711  brsegle  25757  outsideoftr  25778  outsideofeu  25780  funray  25789  funline  25791  lineunray  25796  lineelsb2  25797  ordcmp  25912  itg2addnclem  25958  itg2addnclem2  25959  itg2addnc  25960  itg2gt0cn  25961  itgaddnclem2  25965  nn0prpwlem  26017  nn0prpw  26018  fneval  26059  topfneec  26063  filnetlem4  26102  unirep  26106  f1opr  26118  indexa  26127  sdclem1  26139  fdc  26141  neificl  26151  istotbnd  26170  sstotbnd2  26175  isbnd  26181  isbnd3b  26186  heibor1lem  26210  heiborlem3  26214  rrnheibor  26238  isrngohom  26273  isrngoiso  26286  iscrngo2  26300  isidl  26316  ispridl  26336  pridlidl  26337  pridlnr  26338  pridl  26339  ismaxidl  26342  maxidlidl  26343  smprngopr  26354  prnc  26369  brabsb2  26403  prter3  26423  ralxpxfr2d  26433  isnacs  26450  mzpclval  26474  elmzpcl  26475  mzpcompact2lem  26500  eldiophb  26507  eldioph3  26516  fz1eqin  26519  diophrex  26526  eq0rabdioph  26527  rexrabdioph  26546  dvdsrabdioph  26562  eldioph4b  26564  eldioph4i  26565  elpell1qr  26602  elpell14qr  26604  elpell1234qr  26606  pell1234qrmulcl  26610  rmydioph  26777  rmxdioph  26779  aomclem8  26829  islmodfg  26837  islssfg2  26839  islnm2  26846  frlmelbas  26894  ellspd  26924  islinds  26949  islindf4  26978  hbtlem2  26998  hbtlem5  27002  elmnc  27011  rngunsnply  27048  psgnunilem5  27087  psgnunilem3  27089  psgneldm2  27097  psgneu  27099  issdrg  27175  isdomn3  27193  expgrowth  27222  iotasbc2  27290  fvelrnbf  27358  stoweidlem31  27449  stoweidlem34  27452  stoweidlem59  27477  fnopafvb  27689  afvelrnb  27697  afvelrnb0  27698  vdn0frgrav2  27778  vdgn0frgrav2  27779  frgrancvvdeqlem4  27786  frgrancvvdeqlem7  27789  frgrawopreglem4  27800  trsbc  27969  e2ebind  27994  bnj206  28437  bnj1366  28540  bnj1171  28708  bnj1253  28725  bnj1417  28749  islshp  29095  islsat  29107  islshpat  29133  lcvexchlem1  29150  lsatnem0  29161  islfl  29176  ellkr  29205  lshpsmreu  29225  lshpkrlem3  29228  cvrval2  29390  cvrnbtwn2  29391  cvrnbtwn3  29392  isat  29402  leatb  29408  leat2  29410  cvlsupr2  29459  3dim0  29572  ps-2  29593  islln  29621  islln3  29625  llnexatN  29636  islpln  29645  islpln5  29650  lplnexatN  29678  islvol  29688  islvol5  29694  dalem-cly  29786  isline  29854  ispointN  29857  ispsubsp  29860  linepsubN  29867  elpmap  29873  isline4N  29892  elpadd  29914  paddcom  29928  pmapjoin  29967  pmapjat1  29968  llnexchb2  29984  elpclN  30007  pclcmpatN  30016  ispsubclN  30052  iswatN  30109  islhp  30111  islaut  30198  ispautN  30214  isldil  30225  isltrn  30234  isltrn2N  30235  isdilN  30269  istrnN  30272  cdlemefrs29bpre0  30511  cdleme40v  30584  istendo  30875  diaelval  31149  diaeldm  31152  dibopelvalN  31259  dibopelval2  31261  dib1dim  31281  dibglbN  31282  diblsmopel  31287  dicopelval  31293  dicelvalN  31294  dicelval3  31296  dicvalrelN  31301  diclspsn  31310  dihopelvalcpre  31364  xihopellsmN  31370  dihopellsm  31371  dih1  31402  dihglblem2aN  31409  dihglblem2N  31410  dihmeetlem4preN  31422  dihglb2  31458  dvh2dim  31561  islpolN  31599  lcfl7N  31617  lcdlss  31735  hdmap1fval  31913  hdmapfval  31946  hgmapfval  32005  hdmapglem7a  32046  hdmapoc  32050
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