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  1800  2eu6  2241  abeq2d  2405  necon2bbid  2517  cbvralf  2771  cbvreu  2775  cbvrab  2799  ceqsralt  2824  ralab2  2943  rexab2  2945  reu7  2973  reu8  2974  2reu5  2986  cbvralcsf  3156  cbvreucsf  3158  cbvrabcsf  3159  ralss  3252  rexss  3253  prssg  3786  ssunsn2  3789  eqsn  3791  2ralunsn  3832  eluniab  3855  elintab  3889  dfiun2g  3951  dfiin2g  3952  disjprg  4035  disjxun  4037  cbvopab1  4105  cbvmpt  4126  axsep2  4158  notzfaus  4201  opeqsn  4278  sotrieq2  4358  ordtri2  4443  oneqmini  4459  reusv3  4558  reusv6OLD  4561  reusv7OLD  4562  reuxfrd  4575  elpwunsn  4584  tfisi  4665  frsn  4776  eliunxp  4839  relop  4850  eldm2g  4891  reldm0  4912  relrn0  4953  asymref2  5076  somin1  5095  xpnz  5115  xpcan  5128  xpcan2  5129  cbviota  5240  iota1  5249  sniota  5262  fncnv  5330  fnres  5376  brprcneu  5534  fnopfvb  5580  fvelrnb  5586  funimass4  5589  dffv2  5608  fvopab3g  5614  eqfnfv  5638  eqfnfv3  5640  eqfnfv2f  5642  fvreseq  5644  fnreseql  5651  fniniseg  5662  rexsupp  5666  respreima  5670  rexrn  5683  ralrn  5684  f1ompt  5698  fsn  5712  fconstfv  5750  eufnfv  5768  rexima  5773  ralima  5774  dff13  5799  fliftfun  5827  isocnv  5843  isoini  5851  f1oiso  5864  oprabid  5898  eloprabga  5950  resoprab  5956  eqfnov  5966  eqfnov2  5967  ov6g  6001  ovelrn  6012  funimassov  6013  ovelimab  6014  ndmovg  6019  caovord2  6048  eqop  6178  releldm2  6186  dfoprab4  6193  exopxfr2  6200  fparlem1  6234  fparlem2  6235  xporderlem  6242  poxp  6243  soxp  6244  fnwelem  6246  brtpos2  6256  brtpos0  6257  rntpos  6263  dftpos3  6268  tpostpos  6270  tpossym  6282  tposoprab  6286  opiota  6306  cbvriota  6331  eusvobj2  6353  oevn0  6530  om00el  6590  omordlim  6591  omlimcl  6592  oeoa  6611  oeoe  6613  oeeulem  6615  oeeui  6616  oaabs2  6659  omabs  6661  erth2  6721  qliftfun  6759  erovlem  6770  ecopovsym  6776  th3qlem1  6780  elpmg  6802  elpm2g  6803  map0e  6821  dom2lem  6917  mapsnen  6954  xpdom2  6973  omxpenlem  6979  0sdomg  7006  fodomr  7028  xpf1o  7039  mapen  7041  ac6sfi  7117  marypha2lem3  7206  ordtypelem7  7255  wemaplem1  7277  wemapso2lem  7281  wemapso2  7283  elharval  7293  brwdom3  7312  unwdomg  7314  xpwdomg  7315  inf3lem1  7345  cantnfs  7383  cantnfp1lem2  7397  cantnflem1d  7406  cantnflem1  7407  mapfien  7415  wemapwe  7416  r1sdom  7462  rankr1ai  7486  rankval2  7506  unbndrank  7530  rankunb  7538  tcrank  7570  bnd2  7579  cardnueq0  7613  iscard2  7625  r0weon  7656  fseqenlem1  7667  alephord2  7719  cardaleph  7732  aceq0  7761  dfac5lem4  7769  dfac5  7771  kmlem14  7805  cfsmolem  7912  isfin4-2  7956  fin23lem26  7967  fin23lem22  7969  fin1a2lem7  8048  axdc3lem2  8093  axdc3  8096  zfac  8102  zornn0g  8148  axdclem  8162  brdom3  8169  zfcndac  8257  fpwwe2lem8  8275  fpwwe2lem12  8279  fpwwe2lem13  8280  fpwwe2  8281  pwfseqlem3  8298  winainflem  8331  eltsk2g  8389  inatsk  8416  axgroth2  8463  axgroth6  8466  sstskm  8480  ltexpi  8542  ordpinq  8583  lterpq  8610  ltanq  8611  ltmnq  8612  genpv  8639  genpelv  8640  prlem934  8673  prlem936  8687  addcmpblnr  8710  ltsrpr  8715  ltsosr  8732  mulgt0sr  8743  supsrlem  8749  elreal2  8770  ltresr  8778  ltresr2  8779  axrrecex  8801  axpre-ltadd  8805  axpre-mulgt0  8806  axpre-sup  8807  subcan2  9088  negcon1  9115  negcon2  9116  lt0neg1  9296  lt0neg2  9297  le0neg1  9298  le0neg2  9299  msq0d  9433  divmul2  9444  reclt1  9667  recgt1  9668  fimaxre  9717  infm3  9729  suprlub  9732  suprleub  9734  infmrgelb  9750  addltmul  9963  arch  9978  elznn0  10054  nn0lt10b  10094  recnz  10103  uzindOLD  10122  eluz1  10250  raluz  10283  rexuz  10285  nnwof  10301  cnref1o  10365  ltxr  10473  xrltlen  10496  dflt2  10498  xrrebnd  10513  qbtwnre  10542  xlt0neg1  10562  xlt0neg2  10563  xle0neg1  10564  xle0neg2  10565  xmulneg1  10605  supxrbnd  10663  elixx1  10681  ixxun  10688  elioo2  10713  elicc4  10733  elioopnf  10753  elioomnf  10754  iooneg  10772  iccneg  10773  iccshftr  10785  iccshftl  10787  iccdil  10789  icccntr  10791  iccf1o  10794  elfz1  10803  0fz1  10829  elfzp1  10852  fzpr  10856  fznn0  10867  uzsplit  10871  elfzm1b  10876  elfzp12  10877  fzm1  10878  bernneq  11243  hashbclem  11406  hashfacen  11408  hashf1  11411  2shfti  11591  sqrmsq2i  11887  limsupgle  11967  limsuple  11968  rlim  11985  clim0  11996  ello12  12006  elo12  12017  o1lo1  12027  rlimresb  12055  lo1add  12116  lo1mul  12117  rlimno1  12143  summo  12206  fsumsplit  12228  mertenslem2  12357  xpnnenOLD  12504  cnso  12541  sqr2irr  12543  dvdsval2  12550  alzdvds  12594  odd2np1lem  12602  divalgb  12619  bitsval  12631  bitsmod  12643  sadcp1  12662  gcddvds  12710  bezoutlem3  12735  bezout  12737  isprm3  12783  prmind2  12785  dvdsprime  12787  coprm  12795  prmdvdsexp  12809  crt  12862  pythagtriplem2  12886  pythagtrip  12903  pceu  12915  pc11  12948  vdwapval  13036  vdwapun  13037  vdwlem10  13053  vdwlem12  13055  vdwlem13  13056  ramval  13071  ramub1lem2  13090  prmlem0  13123  elrest  13348  imasleval  13459  ismri  13549  isacs  13569  isacs2  13571  acsfn1  13579  iscatd2  13599  homfeq  13613  catpropd  13628  ismon  13652  issect  13672  issect2  13673  isinv  13678  invsym  13680  isssc  13713  subsubc  13743  isfunc  13754  funcres2b  13787  isnat  13837  fucinv  13863  elhoma  13880  setcinv  13938  isprs  14080  isdrs  14084  istos  14157  tosso  14158  latnle  14207  isipodrs  14280  isacs5  14291  latdisd  14309  isdlat  14312  spwmo  14351  ismhm  14433  issubm  14441  grpsubeq0  14568  grpsubadd  14569  issubg  14637  subgmulg  14651  issubg3  14653  0subg  14658  isnsg  14662  eqger  14683  eqglact  14684  eqgid  14685  isghm  14699  isga  14761  gacan  14775  gaorb  14777  gastacos  14780  orbsta  14783  elcntz  14814  elcntzsn  14817  sscntz  14818  dfod2  14893  isslw  14935  sylow2alem2  14945  lsmelvalx  14967  lsmcom2  14982  lsmass  14995  lssnle  14999  pj1eu  15021  lsmhash  15030  efgi  15044  efgval2  15049  efgtlen  15051  efgred  15073  lsmcomx  15164  iscyggen2  15184  iscyg3  15189  cygabl  15193  gsumval3eu  15206  gsumzsplit  15222  eldprd  15255  subgdmdprd  15285  dprddisj2  15290  dprd2da  15293  dmdprdsplit2lem  15296  dmdprdsplit2  15297  dprdsplit  15299  dmdprdpr  15300  pgpfac1lem3  15328  pgpfac1lem4  15329  pgpfac1lem5  15330  dvdsr02  15454  isunit  15455  isirred  15497  isrhm  15517  drngunit  15533  subsubrg2  15588  issubrg3  15589  isabv  15600  islmod  15647  islss  15708  lsslss  15734  lspsnel  15776  islmhm  15800  lmhmeql  15828  islbs  15845  lsmspsn  15853  lsmelval2  15854  lspprel  15863  lvecvscan2  15881  lvecinv  15882  lspsneq  15891  lspsneu  15892  lspsolvlem  15911  islpidl  16014  lidldvgen  16023  isnzr2  16031  aspval2  16102  mplsubglem  16195  mpllsslem  16196  mplmonmul  16224  opsrtoslem2  16242  prmirredlem  16462  zrhrhmb  16481  zndvds  16519  elocv  16584  iscss  16599  pjdm  16623  ishil2  16635  isobs  16636  obslbs  16646  istop2g  16658  istopon  16679  isbasis2g  16702  isbasis3g  16703  tgss2  16741  bastop1  16747  iscld  16780  elcls  16826  ntreq0  16830  isclo  16840  isclo2  16841  islp  16888  lpdifsn  16891  islpi  16896  restsn  16917  restopn2  16924  restlp  16929  ordtbaslem  16934  ordtbas2  16937  lmbr  17004  cnprest2  17034  ist0-3  17089  ist1-2  17091  cmpsublem  17142  cmpfi  17151  1stcrest  17195  2ndcdisj  17198  1stccnp  17204  llyi  17216  nllyi  17217  lly1stc  17238  iskgen3  17260  kgencn  17267  txbas  17278  eltx  17279  elpt  17283  xkoccn  17329  ptcnplem  17331  hausdiag  17355  hauseqlcld  17356  txlm  17358  txkgen  17362  kqfvima  17437  kqt0lem  17443  r0cld  17445  regr1lem2  17447  hmeoimaf1o  17477  isfbas2  17546  fbssfi  17548  trfbas2  17554  trfil2  17598  fmfnfmlem4  17668  elflim2  17675  flimrest  17694  cnflf  17713  txflf  17717  fclsopn  17725  ufilcmp  17743  cnfcf  17753  alexsubALTlem4  17760  tmdcn2  17788  divstgpopn  17818  divstgplem  17819  eltsms  17831  tsmsgsum  17837  tsmssplit  17850  ismet  17904  isxmet  17905  ismet2  17914  metn0  17940  elbl  17965  metrest  18086  dscmet  18111  nrmmetd  18113  isngp3  18136  nmogelb  18241  isnmhm  18271  qtopbaslem  18283  xrsxmet  18331  icccmplem2  18344  metdseq0  18374  elcncf  18409  cnheibor  18469  ishtpy  18486  isphtpy  18495  isphtpc  18508  om1elbas  18546  elpi1  18559  nmhmcn  18617  iscph  18622  tchcph  18683  lmmbrf  18704  iscfil  18707  iscfil2  18708  iscau  18718  caucfil  18725  iscmet  18726  iscmet3  18735  bcthlem1  18762  minveclem3b  18808  minveclem6  18814  evthicc2  18836  ovolfioo  18843  ovolficc  18844  ovolshftlem1  18884  ovolscalem1  18888  iundisj2  18922  dyadmbl  18971  volsup2  18976  mbfmax  19020  mbfaddlem  19031  mbfsup  19035  mbfinf  19036  i1f1lem  19060  i1fres  19076  itg1climres  19085  mbfi1fseqlem4  19089  itg2leub  19105  itg2seq  19113  itg2splitlem  19119  itg2monolem1  19121  itg2mono  19124  itg2cn  19134  iblpos  19163  iblcn  19169  itgsplit  19206  ellimc2  19243  dvreslem  19275  elcpn  19299  rolle  19353  dvlip  19356  dvivth  19373  tdeglem4  19462  deg1ldg  19494  ply1nzb  19524  ply1divmo  19537  ply1divex  19538  fta1glem2  19568  plyco0  19590  elply  19593  coeeu  19623  plydivex  19693  taylthlem2  19769  radcnvlt1  19810  sincosq1sgn  19882  sincosq2sgn  19883  coseq1  19906  logreclem  20132  affineequiv  20139  dcubic  20158  quart  20173  atans2  20243  efrlim  20280  mumullem2  20434  dvdsflsumcom  20444  fsumvma2  20469  chpchtsum  20474  chpub  20475  dchrelbas  20491  dchrelbas2  20492  dchreq  20513  dchrptlem2  20520  lgsquadlem2  20610  lgsquadlem3  20611  m1lgs  20617  2sqlem6  20624  2sqlem9  20628  2sqlem10  20629  dchrisum0flb  20675  pntpbnd1  20751  pntlem3  20774  pntlemp  20775  isgrpo  20879  isgrpo2  20880  isgrp2d  20918  issubgo  20986  ismgm  21003  rngosn3  21109  nvsubadd  21229  isssp  21316  islno  21347  nmogtmnf  21364  nmoubi  21366  nmounbi  21370  isblo  21376  ishmo  21405  ubthlem1  21465  ubthlem2  21466  minvecolem5  21476  minvecolem6  21477  hvmulcan2  21668  hire  21689  ocel  21876  ocsh  21878  pjhthmo  21897  shscom  21914  shmodsi  21984  elspani  22138  adjsym  22429  eigorthi  22433  nmopgtmnf  22464  adjeu  22485  adjval2  22487  cnvadj  22488  nmopub  22504  nmfnleub  22521  eleigvec  22553  nmop0h  22587  largei  22863  mdbr2  22892  mddmd2  22905  mdsl2i  22918  chrelat3  22967  atnemeq0  22973  chirredlem1  22986  sumdmdii  23011  sumdmdlem  23014  dmdbr5ati  23018  cdjreui  23028  ballotlemodife  23072  preqsnd  23209  cbvmptf  23235  funcnv5mpt  23251  curry2ima  23262  disjabrex  23374  disjabrexf  23375  iundisj2fi  23379  iundisj2f  23381  mbfmcnt  23588  dya2iocrrnval  23597  isibfm  23608  ind1a  23619  elorvc  23675  subfacp1lem3  23728  subfacp1lem5  23730  subfacp1lem6  23731  erdszelem9  23745  erdszelem10  23746  erdsze2lem2  23750  iscvm  23805  cvmlift2lem10  23858  wrdumgra  23883  eupath2lem2  23917  eupath2lem3  23918  snmlval  23929  elgiso  24018  climuzcnv  24019  zmodid2  24025  mulcan2g  24100  mulsuble0b  24103  prodmo  24159  pdivsq  24173  dfpo2  24183  br6  24185  fprb  24200  dfdm5  24203  dfrn5  24204  dfon2lem7  24216  dfon2  24219  dfrdg2  24223  predreseq  24250  wfrlem1  24327  frrlem1  24352  sltval2  24381  sltintdifex  24388  sltres  24389  nofulllem5  24431  dfiota3  24533  brimg  24547  brsuccf  24551  dfrdg4  24560  elee  24594  mptelee  24595  colinearalglem2  24607  colinearalg  24610  ax5seglem5  24633  axeuclidlem  24662  axeuclid  24663  axcontlem1  24664  axcontlem2  24665  axcontlem5  24668  axcontlem7  24670  btwnouttr  24719  btwnexch  24720  funtransport  24726  cgr3permute1  24743  colinearperm1  24757  brsegle  24803  outsideoftr  24824  outsideofeu  24826  funray  24835  funline  24837  lineunray  24842  lineelsb2  24843  ordcmp  24958  itg2addnclem  25003  itg2addnclem2  25004  itg2addnc  25005  itg2gt0cn  25006  itgaddnclem2  25010  copsexgb  25069  dfoprab4pop  25140  elo  25144  splint  25151  cnvref2  25169  eloi  25189  celsor  25214  surjsec2  25223  iscst3  25279  iscst4  25280  puub2  25361  puub  25362  ismxl2  25370  ismnl2  25371  prsubrtr  25502  isidlNEW  25549  vecval1b  25554  svli2  25587  prcnt  25654  cnfilca  25659  limptlimpr2lem1  25677  issubcv  25773  ishomc  25892  ismona  25912  ismonb  25913  isepib  25923  isfunb  25938  issubcata  25949  isntr  25976  islimcat  25979  tartarmap  25991  bisig0  26165  isconcl2b  26201  isibg2  26213  bosser  26270  nn0prpwlem  26341  nn0prpw  26342  dfcon2OLD  26356  fneval  26390  topfneec  26394  filnetlem4  26433  unirep  26452  f1opr  26494  indexa  26515  sdclem1  26556  fdc  26558  neificl  26570  istotbnd  26596  sstotbnd2  26601  isbnd  26607  isbnd3b  26612  heibor1lem  26636  heiborlem3  26640  rrnheibor  26664  isrngohom  26699  isrngoiso  26712  iscrngo2  26726  isidl  26742  ispridl  26762  pridlidl  26763  pridlnr  26764  pridl  26765  ismaxidl  26768  maxidlidl  26769  smprngopr  26780  prnc  26795  brabsb2  26833  prter3  26853  ralxpxfr2d  26863  isnacs  26882  mzpclval  26906  elmzpcl  26907  mzpcompact2lem  26932  eldiophb  26939  eldioph3  26948  fz1eqin  26951  diophrex  26958  eq0rabdioph  26959  rexrabdioph  26978  dvdsrabdioph  26994  eldioph4b  26997  eldioph4i  26998  elpell1qr  27035  elpell14qr  27037  elpell1234qr  27039  pell1234qrmulcl  27043  rmydioph  27210  rmxdioph  27212  aomclem8  27262  islmodfg  27270  islssfg2  27272  islnm2  27279  frlmelbas  27327  ellspd  27357  islinds  27382  islindf4  27411  hbtlem2  27431  hbtlem5  27435  elmnc  27444  rngunsnply  27481  psgnunilem5  27520  psgnunilem3  27522  psgneldm2  27530  psgneu  27532  issdrg  27608  isdomn3  27626  expgrowth  27655  iotasbc2  27723  fvelrnbf  27792  stoweidlem31  27883  fnopafvb  28123  afvelrnb  28131  afvelrnb0  28132  jaoi2  28176  mpt2xopovel  28202  injresinjlem  28214  injresinj  28215  hashtpg  28217  usgra1v  28260  nbgrael  28275  nbgra0nb  28278  nb3graprlem2  28288  nb3grapr2  28290  cusgra2v  28297  uvtxel  28302  trlonprop  28341  0wlk  28343  0trl  28344  fargshiftfo  28383  usgrcyclnl1  28386  trsbc  28603  e2ebind  28628  bnj206  29075  bnj1366  29178  bnj1171  29346  bnj1253  29363  bnj1417  29387  ax12-4  29728  islshp  29791  islsat  29803  islshpat  29829  lcvexchlem1  29846  lsatnem0  29857  islfl  29872  ellkr  29901  lshpsmreu  29921  lshpkrlem3  29924  cvrval2  30086  cvrnbtwn2  30087  cvrnbtwn3  30088  isat  30098  leatb  30104  leat2  30106  cvlsupr2  30155  3dim0  30268  ps-2  30289  islln  30317  islln3  30321  llnexatN  30332  islpln  30341  islpln5  30346  lplnexatN  30374  islvol  30384  islvol5  30390  dalem-cly  30482  isline  30550  ispointN  30553  ispsubsp  30556  linepsubN  30563  elpmap  30569  isline4N  30588  elpadd  30610  paddcom  30624  pmapjoin  30663  pmapjat1  30664  llnexchb2  30680  elpclN  30703  pclcmpatN  30712  ispsubclN  30748  iswatN  30805  islhp  30807  islaut  30894  ispautN  30910  isldil  30921  isltrn  30930  isltrn2N  30931  isdilN  30965  istrnN  30968  cdlemefrs29bpre0  31207  cdleme40v  31280  istendo  31571  diaelval  31845  diaeldm  31848  dibopelvalN  31955  dibopelval2  31957  dib1dim  31977  dibglbN  31978  diblsmopel  31983  dicopelval  31989  dicelvalN  31990  dicelval3  31992  dicvalrelN  31997  diclspsn  32006  dihopelvalcpre  32060  xihopellsmN  32066  dihopellsm  32067  dih1  32098  dihglblem2aN  32105  dihglblem2N  32106  dihmeetlem4preN  32118  dihglb2  32154  dvh2dim  32257  islpolN  32295  lcfl7N  32313  lcdlss  32431  hdmap1fval  32609  hdmapfval  32642  hgmapfval  32701  hdmapglem7a  32742  hdmapoc  32746
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