Theorem syl6bb 536

Description: A syllogism inference from two biconditionals.

Hypotheses

Ref	Expression
syl6bb.1	|- (ph -> (ps <-> ch))
syl6bb.2	|- (ch <-> th)

Assertion

Ref	Expression
syl6bb	|- (ph -> (ps <-> th))

Proof of Theorem syl6bb

Step	Hyp	Ref	Expression
1		syl6bb.1	. 2 |- (ph -> (ps <-> ch))
2		syl6bb.2	. . 3 |- (ch <-> th)
3	2	a1i 8	. 2 |- (ph -> (ch <-> th))
4	1, 3	bitrd 528	1 |- (ph -> (ps <-> th))

Syntax hints:   -> wi 3   <-> wb 146

This theorem is referenced by:  syl6rbb 537  syl6bbr 538  3bitr3g 554  biantrurd 727  19.17 1049  19.33b 1092  2eu6 1454  abeq2d 1572  necon2bbid 1623  eqvinc 1883  eueq3 1919  reu7 1935  reu8 1936  sbcralt 1990  sbcralgf 1992  uniiunlem 2132  reldisj 2313  eqsn 2474  eluniab 2513  elintab 2544  dfiun2g 2586  axsep2 2704  notzfaus 2741  sbcsng 2753  moabex 2766  opeqsn 2802  sotrieq2 2862  reuxfr 2904  elpwunsn 2912  ordtri2 2982  ordtri4 2984  oneqmini 3017  ordtri2or 3077  ralxp 3218  relop 3275  opelcog 3290  opelcnvg 3296  dmsnop 3328  reldm0 3331  relrn0 3356  iss 3397  asymref2 3440  xpnz 3466  fncnv 3561  fvprc 3721  fnopfvb 3754  funopfvb 3756  fvelrnb 3760  funimass4 3763  fvopab3 3777  fvopabn 3786  eqfnfvf 3798  elrnopabg 3800  fsn 3834  fconstfv 3849  funiunfv 3866  f1fv 3874  f1ocnvfv3 3883  isocnv 3896  isoini 3900  f1oiso 3904  eloprabg 4007  resoprab 4009  eqfnoprval 4016  oprabval6g 4032  oprvalelrn 4039  caoprord2 4057  2ndconst 4097  elopabi 4117  eloprabi 4118  elrnoprabg 4124  oevn0 4154  om00el 4207  omordlim 4208  omlimcl 4209  ecopoprsym 4310  th3qlem1 4314  dom2d 4403  mapsnen 4428  undom 4436  xpdom2 4440  pw2en 4444  0sdomg 4464  fodomr 4481  mapdom2 4492  mapxpen 4493  xpmapenlem5 4498  unfilem1 4543  abfii4 4556  fodomfi 4558  inf3lem1 4605  r1tr 4646  rankval2 4662  rankr1 4666  rankval3 4673  unbndrank 4675  r1pwcl 4679  bnd2 4716  aceq0 4722  aceq5lem4 4730  aceq5 4732  axac 4737  ac6lem 4746  kmlem14 4770  iscard2 4846  alephord2 4868  cardaleph 4877  zfcndac 4963  ltexpi 5021  mulcmpblnq 5045  ordpipq 5048  ltsopq 5067  genpelv 5095  genpprecl 5096  genpnnp 5100  genpass 5104  distrlem1pr 5119  distrlem5pr 5123  prlem936a 5145  addcmpblnr 5173  ltsrpr 5178  ltsosr 5195  mulgt0sr 5206  map2psrpr 5212  ltresr 5250  axrnegex 5275  axrrecex 5276  pre-axltadd 5281  pre-axmulgt0 5282  negcon1t 5402  negcon2t 5403  xrrebndt 5560  lt0neg1t 5659  lt0neg2t 5660  le0neg1t 5661  le0neg2t 5662  divmul2t 5696  reclt1t 5886  recgt1t 5887  infm3 6042  arch 6059  supxrbnd 6079  nn0ltp1let 6115  elznn0 6137  elnnz1 6143  elnn0nn 6159  zltp1let 6169  recnzt 6179  dfuz 6190  uzindOLD 6196  uzwo3lem2 6205  seq1lem2 6296  iooint 6358  elioo1t 6364  elioo2t 6365  elioo3g 6366  elioc1t 6367  elico1t 6368  elicc1t 6369  elioo4g 6371  ioonegt 6392  iccnegt 6393  icounlem 6398  snunioolem 6400  ioojoint 6402  eluz1t 6406  raluz 6428  rexuz 6430  elfz1t 6456  elfz2t 6458  elfzuzb 6462  elfzuz2t 6472  elfz2nn0t 6481  fznn0t 6502  exple1t 6593  bernneq 6638  sqr2irrlem3 6712  crulem 6722  creur 6728  creui 6729  abssubne0t 6867  cvg2 6907  dffsum 6983  fsumrev 7014  fsumshft 7016  clm1 7062  clmnns 7069  climshft 7089  climres 7090  caucvg 7148  caucvg3t 7153  dfisum 7176  acdc3 7472  acdc2 7475  acdc5 7478  acdc 7480  xpnnen 7484  infxpidmlem5 7541  infxpidmlem10 7546  istop2g 7582  isbasis2g 7597  isbasis3g 7598  eltg3t 7611  tgss3t 7623  elcls 7689  ntreq0 7693  islp 7729  islp2 7732  islpi 7734  cncnplem3 7761  cncnplem4 7762  ismet 7783  elbl 7823  blrn2 7827  blss 7838  metcnplem 7871  cncfmet 7890  dscmet 7903  lmbr2 7914  iscau2 7922  iscau5 7926  lmbrnns 7927  iscaunns 7929  metcn4 7956  isgrp 8026  issubg 8101  nvsubadd 8260  sspval 8367  isssp 8368  islno 8399  nmogtmnf 8418  nmounbi 8424  isblo 8427  ubthlem1 8514  spwmo 8641  pilem1 8656  sincosq1sgn 8689  sincosq2sgn 8690  efghgrpilem 8704  efif1lem5 8719  axgroth2 8763  grothinf 8766  hvmulcan2t 8925  hiret 8945  ocelt 9139  ocsh 9141  chocuni 9157  shselt 9263  shscomt 9268  shmods 9347  elspan 9451  adjsymt 9744  eigorth 9748  nmopgtmnf 9780  adjval2t 9800  cnvadj 9801  hhlno 9811  elnlfnt 9837  eleigvect 9866  nmop0h 9901  large 10179  mdbr2 10208  mddmd 10221  mdsl2 10234  chrelat3t 10283  atnem0 10289  irredlem1 10302  sumdmdi 10327  sumdmdlem 10330  dmdbr5at 10334  cdjreu 10344  elgiso 10383  uninqs 10425  elo 10428  cnfilca 10537  rcfpfillem3 10540  rcfpfillem6 10543  plimfil 10552  eloi 10602  ishomc 10660  ismona 10678  ishgrag 10705

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain