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

Theorem syl6bb 254
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 246 1  |-  ( ph  ->  ( ps  <->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178
This theorem is referenced by:  syl6rbb  255  syl6bbr  256  3bitr3g  280  bibi2i  306  ibibr  334  pm5.75  905  jaoi2  935  cadan  1402  19.17  1885  2eu6  2368  abeq2d  2547  necon2bbid  2664  cbvralf  2928  cbvreu  2932  cbvrab  2956  ceqsralt  2981  ralab2  3101  rexab2  3103  reu7  3131  reu8  3132  2reu5  3144  cbvralcsf  3313  cbvreucsf  3315  cbvrabcsf  3316  ralss  3411  rexss  3412  prssg  3955  ssunsn2  3960  eqsn  3962  2ralunsn  4006  eluniab  4029  elintab  4063  dfiun2g  4125  dfiin2g  4126  disjprg  4211  disjxun  4213  cbvopab1  4281  cbvmpt  4302  axsep2  4334  notzfaus  4377  opeqsn  4455  sotrieq2  4534  ordtri2  4619  oneqmini  4635  reusv3  4734  reusv6OLD  4737  reusv7OLD  4738  reuxfrd  4751  elpwunsn  4760  tfisi  4841  frsn  4951  eliunxp  5015  relop  5026  eldm2g  5069  reldm0  5090  relrn0  5131  asymref2  5254  somin1  5273  xpnz  5295  xpcan  5308  xpcan2  5309  cbviota  5426  iota1  5435  sniota  5448  fncnv  5518  fnres  5564  brprcneu  5724  fnopfvb  5771  fvelrnb  5777  funimass4  5780  dffv2  5799  fvopab3g  5805  eqfnfv  5830  eqfnfv3  5832  eqfnfv2f  5834  fvreseq  5836  fnreseql  5843  fniniseg  5854  rexsupp  5858  respreima  5862  rexrn  5875  ralrn  5876  f1ompt  5894  fsn  5909  fconstfv  5957  eufnfv  5975  rexima  5980  ralima  5981  dff13  6007  fliftfun  6037  isocnv  6053  isoini  6061  f1oiso  6074  oprabid  6108  eloprabga  6163  resoprab  6169  eqfnov  6179  eqfnov2  6180  ov6g  6214  ovelrn  6225  funimassov  6226  ovelimab  6227  ndmovg  6233  caovord2  6262  eqop  6392  releldm2  6400  dfoprab4  6407  exopxfr2  6414  bropopvvv  6429  fparlem1  6449  fparlem2  6450  xporderlem  6460  poxp  6461  soxp  6462  fnwelem  6464  mpt2xopovel  6474  brtpos2  6488  brtpos0  6489  rntpos  6495  dftpos3  6500  tpostpos  6502  tpossym  6514  tposoprab  6518  opiota  6538  cbvriota  6563  eusvobj2  6585  oevn0  6762  om00el  6822  omordlim  6823  omlimcl  6824  oeoa  6843  oeoe  6845  oeeulem  6847  oeeui  6848  oaabs2  6891  omabs  6893  erth2  6953  qliftfun  6992  erovlem  7003  ecopovsym  7009  th3qlem1  7013  elpmg  7035  elpm2g  7036  map0e  7054  dom2lem  7150  mapsnen  7187  xpdom2  7206  omxpenlem  7212  0sdomg  7239  fodomr  7261  xpf1o  7272  mapen  7274  ac6sfi  7354  marypha2lem3  7445  ordtypelem7  7496  wemaplem1  7518  wemapso2lem  7522  wemapso2  7524  elharval  7534  brwdom3  7553  unwdomg  7555  xpwdomg  7556  inf3lem1  7586  cantnfs  7624  cantnfp1lem2  7638  cantnflem1d  7647  cantnflem1  7648  mapfien  7656  wemapwe  7657  r1sdom  7703  rankr1ai  7727  rankval2  7747  unbndrank  7771  rankunb  7779  tcrank  7813  bnd2  7822  cardnueq0  7856  iscard2  7868  r0weon  7899  fseqenlem1  7910  alephord2  7962  cardaleph  7975  aceq0  8004  dfac5lem4  8012  dfac5  8014  kmlem14  8048  cfsmolem  8155  isfin4-2  8199  fin23lem26  8210  fin23lem22  8212  fin1a2lem7  8291  axdc3lem2  8336  axdc3  8339  zfac  8345  zornn0g  8390  axdclem  8404  brdom3  8411  zfcndac  8499  fpwwe2lem8  8517  fpwwe2lem12  8521  fpwwe2lem13  8522  fpwwe2  8523  pwfseqlem3  8540  winainflem  8573  eltsk2g  8631  inatsk  8658  axgroth2  8705  axgroth6  8708  sstskm  8722  ltexpi  8784  ordpinq  8825  lterpq  8852  ltanq  8853  ltmnq  8854  genpv  8881  genpelv  8882  prlem934  8915  prlem936  8929  addcmpblnr  8952  ltsrpr  8957  ltsosr  8974  mulgt0sr  8985  supsrlem  8991  elreal2  9012  ltresr  9020  ltresr2  9021  axrrecex  9043  axpre-ltadd  9047  axpre-mulgt0  9048  axpre-sup  9049  subcan2  9331  negcon1  9358  negcon2  9359  lt0neg1  9539  lt0neg2  9540  le0neg1  9541  le0neg2  9542  msq0d  9676  divmul2  9687  reclt1  9910  recgt1  9911  fimaxre  9960  infm3  9972  suprlub  9975  suprleub  9977  infmrgelb  9993  addltmul  10208  arch  10223  elznn0  10301  nn0lt10b  10341  recnz  10350  uzindOLD  10369  eluz1  10497  raluz  10530  rexuz  10532  nnwof  10548  cnref1o  10612  ltxr  10720  xrltlen  10744  dflt2  10746  xrrebnd  10761  qbtwnre  10790  xlt0neg1  10810  xlt0neg2  10811  xle0neg1  10812  xle0neg2  10813  xmulneg1  10853  supxrbnd  10912  elixx1  10930  ixxun  10937  elioo2  10962  elicc4  10982  elioopnf  11003  elioomnf  11004  iooneg  11022  iccneg  11023  iccshftr  11035  iccshftl  11037  iccdil  11039  icccntr  11041  iccf1o  11044  elfz1  11053  0fz1  11079  elfzp1  11102  fzpr  11106  fznn0  11118  uzsplit  11123  elfzm1b  11130  elfzp12  11131  fzm1  11132  injresinjlem  11204  injresinj  11205  bernneq  11510  hasheqf1o  11638  hashtpg  11696  hashbclem  11706  hashfacen  11708  hashf1  11711  2shfti  11900  sqrmsq2i  12196  limsupgle  12276  limsuple  12277  rlim  12294  clim0  12305  ello12  12315  elo12  12326  o1lo1  12336  rlimresb  12364  lo1add  12425  lo1mul  12426  rlimno1  12452  summo  12516  fsumsplit  12538  mertenslem2  12667  xpnnenOLD  12814  cnso  12851  sqr2irr  12853  dvdsval2  12860  alzdvds  12904  odd2np1lem  12912  divalgb  12929  bitsval  12941  bitsmod  12953  sadcp1  12972  gcddvds  13020  bezoutlem3  13045  bezout  13047  isprm3  13093  prmind2  13095  dvdsprime  13097  coprm  13105  prmdvdsexp  13119  crt  13172  pythagtriplem2  13196  pythagtrip  13213  pceu  13225  pc11  13258  vdwapval  13346  vdwapun  13347  vdwlem10  13363  vdwlem12  13365  vdwlem13  13366  ramval  13381  ramub1lem2  13400  prmlem0  13433  elrest  13660  imasleval  13771  ismri  13861  isacs  13881  isacs2  13883  acsfn1  13891  iscatd2  13911  homfeq  13925  catpropd  13940  ismon  13964  issect  13984  issect2  13985  isinv  13990  invsym  13992  isssc  14025  subsubc  14055  isfunc  14066  funcres2b  14099  isnat  14149  fucinv  14175  elhoma  14192  setcinv  14250  isprs  14392  isdrs  14396  istos  14469  tosso  14470  latnle  14519  isipodrs  14592  isacs5  14603  latdisd  14621  isdlat  14624  spwmo  14663  ismhm  14745  issubm  14753  grpsubeq0  14880  grpsubadd  14881  issubg  14949  subgmulg  14963  issubg3  14965  0subg  14970  isnsg  14974  eqger  14995  eqglact  14996  eqgid  14997  isghm  15011  isga  15073  gacan  15087  gaorb  15089  gastacos  15092  orbsta  15095  elcntz  15126  elcntzsn  15129  sscntz  15130  dfod2  15205  isslw  15247  sylow2alem2  15257  lsmelvalx  15279  lsmcom2  15294  lsmass  15307  lssnle  15311  pj1eu  15333  lsmhash  15342  efgi  15356  efgval2  15361  efgtlen  15363  efgred  15385  lsmcomx  15476  iscyggen2  15496  iscyg3  15501  cygabl  15505  gsumval3eu  15518  gsumzsplit  15534  eldprd  15567  subgdmdprd  15597  dprddisj2  15602  dprd2da  15605  dmdprdsplit2lem  15608  dmdprdsplit2  15609  dprdsplit  15611  dmdprdpr  15612  pgpfac1lem3  15640  pgpfac1lem4  15641  pgpfac1lem5  15642  dvdsr02  15766  isunit  15767  isirred  15809  isrhm  15829  drngunit  15845  subsubrg2  15900  issubrg3  15901  isabv  15912  islmod  15959  islss  16016  lsslss  16042  lspsnel  16084  islmhm  16108  lmhmeql  16136  islbs  16153  lsmspsn  16161  lsmelval2  16162  lspprel  16171  lvecvscan2  16189  lvecinv  16190  lspsneq  16199  lspsneu  16200  lspsolvlem  16219  islpidl  16322  lidldvgen  16331  isnzr2  16339  aspval2  16410  mplsubglem  16503  mpllsslem  16504  mplmonmul  16532  opsrtoslem2  16550  prmirredlem  16778  zrhrhmb  16797  zndvds  16835  elocv  16900  iscss  16915  pjdm  16939  ishil2  16951  isobs  16952  obslbs  16962  istop2g  16974  istopon  16995  isbasis2g  17018  isbasis3g  17019  tgss2  17057  bastop1  17063  iscld  17096  elcls  17142  ntreq0  17146  isclo  17156  isclo2  17157  islp  17209  lpdifsn  17212  islpi  17218  restsn  17239  restopn2  17246  restlp  17252  ordtbaslem  17257  ordtbas2  17260  lmbr  17327  cnprest2  17359  ist0-3  17414  ist1-2  17416  cmpsublem  17467  cmpfi  17476  1stcrest  17521  2ndcdisj  17524  1stccnp  17530  llyi  17542  nllyi  17543  lly1stc  17564  iskgen3  17586  kgencn  17593  txbas  17604  eltx  17605  elpt  17609  xkoccn  17656  ptcnplem  17658  hausdiag  17682  hauseqlcld  17683  txlm  17685  txkgen  17689  kqfvima  17767  kqt0lem  17773  r0cld  17775  regr1lem2  17777  hmeoimaf1o  17807  isfbas2  17872  fbssfi  17874  trfbas2  17880  trfil2  17924  fmfnfmlem4  17994  elflim2  18001  flimrest  18020  cnflf  18039  txflf  18043  fclsopn  18051  ufilcmp  18069  cnfcf  18079  alexsubALTlem4  18086  cnextf  18102  tmdcn2  18124  divstgpopn  18154  divstgplem  18155  eltsms  18167  tsmsgsum  18173  tsmssplit  18186  elutop  18268  ustuqtop  18281  utopsnneiplem  18282  isusp  18296  isucn  18313  iscfilu  18323  ispsmet  18340  ismet  18358  isxmet  18359  ismet2  18368  metn0  18395  elblps  18422  elbl  18423  metrest  18559  metuel2  18614  metutopOLD  18617  psmetutop  18618  restmetu  18622  dscmet  18625  nrmmetd  18627  isngp3  18650  nmogelb  18755  isnmhm  18785  qtopbaslem  18797  xrsxmet  18845  icccmplem2  18859  metdseq0  18889  elcncf  18924  cnheibor  18985  ishtpy  19002  isphtpy  19011  isphtpc  19024  om1elbas  19062  elpi1  19075  nmhmcn  19133  iscph  19138  tchcph  19199  lmmbrf  19220  iscfil  19223  iscfil2  19224  iscau  19234  caucfil  19241  iscmet  19242  iscmet3  19251  cfilucfil3OLD  19276  cfilucfil3  19277  bcthlem1  19282  minveclem3b  19334  minveclem6  19340  evthicc2  19362  ovolfioo  19369  ovolficc  19370  ovolshftlem1  19410  ovolscalem1  19414  iundisj2  19448  dyadmbl  19497  volsup2  19502  mbfmax  19544  mbfaddlem  19555  mbfsup  19559  mbfinf  19560  i1f1lem  19584  i1fres  19600  itg1climres  19609  mbfi1fseqlem4  19613  itg2leub  19629  itg2seq  19637  itg2splitlem  19643  itg2monolem1  19645  itg2mono  19648  itg2cn  19658  iblpos  19687  iblcn  19693  itgsplit  19730  ellimc2  19769  dvreslem  19801  elcpn  19825  rolle  19879  dvlip  19882  dvivth  19899  tdeglem4  19988  deg1ldg  20020  ply1nzb  20050  ply1divmo  20063  ply1divex  20064  fta1glem2  20094  plyco0  20116  elply  20119  coeeu  20149  plydivex  20219  taylthlem2  20295  radcnvlt1  20339  sincosq1sgn  20411  sincosq2sgn  20412  coseq1  20435  logreclem  20665  affineequiv  20672  dcubic  20691  quart  20706  atans2  20776  efrlim  20813  mumullem2  20968  dvdsflsumcom  20978  fsumvma2  21003  chpchtsum  21008  chpub  21009  dchrelbas  21025  dchrelbas2  21026  dchreq  21047  dchrptlem2  21054  lgsquadlem2  21144  lgsquadlem3  21145  m1lgs  21151  2sqlem6  21158  2sqlem9  21162  2sqlem10  21163  dchrisum0flb  21209  pntpbnd1  21285  pntlem3  21308  pntlemp  21309  wrdumgra  21356  usgra1v  21414  usgrafisindb1  21428  nbgraop1  21442  nbgrael  21443  nbgra0nb  21446  nbgraf1olem3  21458  nbgraf1olem5  21460  nb3graprlem2  21466  nb3grapr2  21468  cusgra2v  21476  uvtxel  21503  0wlk  21550  0trl  21551  is2wlk  21570  isspthonpth  21589  fargshiftfo  21630  usgrcyclnl1  21632  dfconngra1  21663  eupath2lem2  21705  eupath2lem3  21706  isgrpo  21789  isgrpo2  21790  isgrp2d  21828  issubgo  21896  ismgm  21913  rngosn3  22019  nvsubadd  22141  isssp  22228  islno  22259  nmogtmnf  22276  nmoubi  22278  nmounbi  22282  isblo  22288  ishmo  22317  ubthlem1  22377  ubthlem2  22378  minvecolem5  22388  minvecolem6  22389  hvmulcan2  22580  hire  22601  ocel  22788  ocsh  22790  pjhthmo  22809  shscom  22826  shmodsi  22896  elspani  23050  adjsym  23341  eigorthi  23345  nmopgtmnf  23376  adjeu  23397  adjval2  23399  cnvadj  23400  nmopub  23416  nmfnleub  23433  eleigvec  23465  nmop0h  23499  largei  23775  mdbr2  23804  mddmd2  23817  mdsl2i  23830  chrelat3  23879  atnemeq0  23885  chirredlem1  23898  sumdmdii  23923  sumdmdlem  23926  dmdbr5ati  23930  cdjreui  23940  preqsnd  24005  disjabrex  24029  disjabrexf  24030  iundisj2f  24035  ofpreima  24086  funcnv5mpt  24089  1stpreima  24100  curry2ima  24102  iundisj2fi  24158  toslub  24196  tosglb  24197  isarchi2  24260  cnvordtrestixx  24316  lmdvg  24343  ind1a  24423  braew  24598  ismbfm  24607  mbfmcnt  24623  issibf  24653  elorvc  24722  ballotlemfc0  24755  ballotlemfcc  24756  ballotlemodife  24760  subfacp1lem3  24873  subfacp1lem5  24875  subfacp1lem6  24876  erdszelem9  24890  erdszelem10  24891  erdsze2lem2  24895  iscvm  24951  cvmlift2lem10  25004  snmlval  25023  elgiso  25112  climuzcnv  25113  zmodid2  25119  mulcan2g  25195  mulsuble0b  25198  prodmo  25267  fprodsplit  25294  fprod2dlem  25309  pdivsq  25373  dfpo2  25383  br6  25385  fprb  25402  dfdm5  25405  dfrn5  25406  dfon2lem7  25421  dfon2  25424  dfrdg2  25428  predreseq  25459  wfrlem1  25543  frrlem1  25587  sltval2  25616  sltintdifex  25623  sltres  25624  nofulllem5  25666  elfuns  25765  dfiota3  25773  brimg  25787  brsuccf  25791  dfrdg4  25800  elee  25838  mptelee  25839  colinearalglem2  25851  colinearalg  25854  ax5seglem5  25877  axeuclidlem  25906  axeuclid  25907  axcontlem1  25908  axcontlem2  25909  axcontlem5  25912  axcontlem7  25914  btwnouttr  25963  btwnexch  25964  funtransport  25970  cgr3permute1  25987  colinearperm1  26001  brsegle  26047  outsideoftr  26068  outsideofeu  26070  funray  26079  funline  26081  lineunray  26086  lineelsb2  26087  ordcmp  26202  heicant  26253  mblfinlem1  26255  ismblfin  26259  mbfresfi  26265  itg2addnclem  26270  itg2addnclem2  26271  itg2addnc  26273  itg2gt0cn  26274  ftc1anclem6  26299  nn0prpwlem  26339  nn0prpw  26340  fneval  26381  topfneec  26385  filnetlem4  26424  unirep  26428  f1opr  26440  indexa  26449  sdclem1  26461  fdc  26463  neificl  26473  istotbnd  26492  sstotbnd2  26497  isbnd  26503  isbnd3b  26508  heibor1lem  26532  heiborlem3  26536  rrnheibor  26560  isrngohom  26595  isrngoiso  26608  iscrngo2  26622  isidl  26638  ispridl  26658  pridlidl  26659  pridlnr  26660  pridl  26661  ismaxidl  26664  maxidlidl  26665  smprngopr  26676  prnc  26691  brabsb2  26725  prter3  26745  ralxpxfr2d  26755  isnacs  26772  mzpclval  26796  elmzpcl  26797  mzpcompact2lem  26822  eldiophb  26829  eldioph3  26838  fz1eqin  26841  diophrex  26848  eq0rabdioph  26849  rexrabdioph  26868  dvdsrabdioph  26884  eldioph4b  26886  eldioph4i  26887  elpell1qr  26924  elpell14qr  26926  elpell1234qr  26928  pell1234qrmulcl  26932  rmydioph  27099  rmxdioph  27101  aomclem8  27150  islmodfg  27158  islssfg2  27160  islnm2  27167  frlmelbas  27215  ellspd  27245  islinds  27270  islindf4  27299  hbtlem2  27319  hbtlem5  27323  elmnc  27332  rngunsnply  27369  psgnunilem5  27408  psgnunilem3  27410  psgneldm2  27418  psgneu  27420  issdrg  27496  isdomn3  27514  expgrowth  27543  iotasbc2  27611  fvelrnbf  27679  stoweidlem31  27770  stoweidlem34  27773  stoweidlem59  27798  fnopafvb  28009  afvelrnb  28017  afvelrnb0  28018  elovmpt3rab1  28107  2ffzoeq  28163  euhash1  28190  cshwssizelem1  28314  usgra2wlkspthlem1  28344  usgra2wlkspthlem2  28345  usgra2pthlem1  28348  iswwlk  28365  iswwlkn  28366  el2wlkonot  28401  el2spthonot  28402  2wlkonot3v  28407  2spthonot3v  28408  usg2spthonot0  28421  usg2spthonot1  28422  vdn0frgrav2  28488  vdgn0frgrav2  28489  frgrancvvdeqlem4  28496  frgrancvvdeqlem7  28499  frgrawopreglem4  28510  frg2wot1  28520  frg2woteqm  28522  2spotmdisj  28531  frgregordn0  28533  trsbc  28699  e2ebind  28724  bnj206  29172  bnj1366  29275  bnj1171  29443  bnj1253  29460  bnj1417  29484  ax7w14lemAUX7  29743  islshp  29851  islsat  29863  islshpat  29889  lcvexchlem1  29906  lsatnem0  29917  islfl  29932  ellkr  29961  lshpsmreu  29981  lshpkrlem3  29984  cvrval2  30146  cvrnbtwn2  30147  cvrnbtwn3  30148  isat  30158  leatb  30164  leat2  30166  cvlsupr2  30215  3dim0  30328  ps-2  30349  islln  30377  islln3  30381  llnexatN  30392  islpln  30401  islpln5  30406  lplnexatN  30434  islvol  30444  islvol5  30450  dalem-cly  30542  isline  30610  ispointN  30613  ispsubsp  30616  linepsubN  30623  elpmap  30629  isline4N  30648  elpadd  30670  paddcom  30684  pmapjoin  30723  pmapjat1  30724  llnexchb2  30740  elpclN  30763  pclcmpatN  30772  ispsubclN  30808  iswatN  30865  islhp  30867  islaut  30954  ispautN  30970  isldil  30981  isltrn  30990  isltrn2N  30991  isdilN  31025  istrnN  31028  cdlemefrs29bpre0  31267  cdleme40v  31340  istendo  31631  diaelval  31905  diaeldm  31908  dibopelvalN  32015  dibopelval2  32017  dib1dim  32037  dibglbN  32038  diblsmopel  32043  dicopelval  32049  dicelvalN  32050  dicelval3  32052  dicvalrelN  32057  diclspsn  32066  dihopelvalcpre  32120  xihopellsmN  32126  dihopellsm  32127  dih1  32158  dihglblem2aN  32165  dihglblem2N  32166  dihmeetlem4preN  32178  dihglb2  32214  dvh2dim  32317  islpolN  32355  lcfl7N  32373  lcdlss  32491  hdmap1fval  32669  hdmapfval  32702  hgmapfval  32761  hdmapglem7a  32802  hdmapoc  32806
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator