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 4404  mapsnen 4429  undom 4438  xpdom2 4442  pw2en 4446  0sdomg 4466  fodomr 4483  mapdom2 4494  mapxpen 4495  xpmapenlem5 4500  unfilem1 4548  abfii4OLD 4564  fodomfiOLD 4566  inf3lem1 4613  r1tr 4654  rankval2 4670  rankr1 4674  rankval3 4681  unbndrank 4683  r1pwcl 4687  bnd2 4724  aceq0 4730  aceq5lem4 4738  aceq5 4740  axac 4745  ac6lem 4754  kmlem14 4778  iscard2 4854  alephord2 4876  cardaleph 4885  zfcndac 4971  ltexpi 5029  mulcmpblnq 5053  ordpipq 5056  ltsopq 5075  genpelv 5103  genpprecl 5104  genpnnp 5108  genpass 5112  distrlem1pr 5127  distrlem5pr 5131  prlem936a 5153  addcmpblnr 5181  ltsrpr 5186  ltsosr 5203  mulgt0sr 5214  map2psrpr 5220  ltresr 5258  axrnegex 5283  axrrecex 5284  pre-axltadd 5289  pre-axmulgt0 5290  negcon1t 5410  negcon2t 5411  xrrebndt 5568  lt0neg1t 5668  lt0neg2t 5669  le0neg1t 5670  le0neg2t 5671  divmul2t 5708  reclt1t 5898  recgt1t 5899  infm3 6054  arch 6071  supxrbnd 6091  nn0ltp1let 6127  elznn0 6149  elnnz1 6155  elnn0nn 6171  zltp1let 6181  recnzt 6191  dfuz 6202  uzindOLD 6208  uzwo3lem2 6217  seq1lem2 6310  iooint 6372  elioo1t 6378  elioo2t 6379  elioo3g 6380  elioc1t 6381  elico1t 6382  elicc1t 6383  elioo4g 6385  ioonegt 6406  iccnegt 6407  icounlem 6412  snunioolem 6414  ioojoint 6416  eluz1t 6420  raluz 6442  rexuz 6444  elfz1t 6470  elfz2t 6472  elfzuzb 6476  elfzuz2t 6486  elfz2nn0t 6495  fznn0t 6516  exple1t 6607  bernneq 6652  sqr2irrlem3 6726  crulem 6736  creur 6742  creui 6743  abssubne0t 6882  cvg2 6922  dffsum 6998  fsumrev 7029  fsumshft 7031  clm1 7077  clmnns 7084  climshft 7104  climres 7105  caucvg 7163  caucvg3t 7168  dfisum 7191  acdc3 7487  acdc2 7490  acdc5 7493  acdc 7495  xpnnen 7499  infxpidmlem5 7556  infxpidmlem10 7561  istop2gOLD 7597  isbasis2g 7612  isbasis3g 7613  eltg3t 7626  tgss3t 7638  elcls 7704  ntreq0 7708  islp 7744  islp2 7747  islpi 7749  cncnplem3 7776  cncnplem4 7777  ismet 7798  elbl 7838  blrn2 7842  blss 7853  metcnplem 7886  cncfmet 7905  dscmet 7918  lmbr2 7929  iscau2 7937  iscau5 7941  lmbrnns 7942  iscaunns 7944  metcn4 7971  isgrp 8041  issubg 8116  nvsubadd 8275  sspval 8382  isssp 8383  islno 8414  nmogtmnf 8433  nmounbi 8439  isblo 8442  ubthlem1 8529  spwmo 8656  pilem1 8671  sincosq1sgn 8704  sincosq2sgn 8705  efghgrpilem 8719  efif1lem5 8734  axgroth2 8778  grothinf 8781  hvmulcan2t 8940  hiret 8960  ocelt 9154  ocsh 9156  chocuni 9172  shselt 9278  shscomt 9283  shmods 9362  elspan 9466  adjsymt 9759  eigorth 9763  nmopgtmnf 9795  adjval2t 9815  cnvadj 9816  hhlno 9826  elnlfnt 9852  eleigvect 9881  nmop0h 9916  large 10194  mdbr2 10223  mddmd 10236  mdsl2 10249  chrelat3t 10298  atnem0 10304  irredlem1 10317  sumdmdi 10342  sumdmdlem 10345  dmdbr5at 10349  cdjreu 10359  elgiso 10398  uninqs 10441  elo 10444  cnfilca 10583  cnfilcaOLD 10584  rcfpfillem3 10589  rcfpfillem3OLD 10590  rcfpfillem6 10595  rcfpfillem6OLD 10596  plimfilOLD 10609  eloi 10659  ishomc 10717  ismona 10737  ishgrag 10769

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