Theorem syl6bb 538

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 530	1 |- (ph -> (ps <-> th))

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

This theorem is referenced by:  syl6rbb 539  syl6bbr 540  3bitr3g 556  biantrurd 729  19.17 1051  19.33b 1094  2eu6 1457  abeq2d 1575  necon2bbid 1626  eqvinc 1886  eueq3 1922  reu7 1938  reu8 1939  sbcralt 1993  sbcralgf 1995  uniiunlem 2135  reldisj 2317  eqsn 2478  eluniab 2517  elintab 2548  dfiun2g 2590  axsep2 2709  notzfaus 2746  sbcsng 2759  moabex 2772  opeqsn 2808  sotrieq2 2868  reuxfr 2910  elpwunsn 2918  ordtri2 2988  ordtri4 2990  oneqmini 3023  ordtri2or 3083  ralxp 3224  relop 3281  opelcog 3296  opelcnvg 3302  dmsnop 3334  reldm0 3337  relrn0 3362  iss 3403  asymref2 3446  xpnz 3472  fncnv 3567  fvprc 3727  fnopfvb 3760  funopfvb 3762  fvelrnb 3766  funimass4 3769  fvopab3 3783  fvopabn 3792  eqfnfvf 3804  elrnopabg 3806  fsn 3840  fconstfv 3855  funiunfv 3872  f1fv 3880  f1ocnvfv3 3889  isocnv 3902  isoini 3906  f1oiso 3910  eloprabg 4013  resoprab 4015  eqfnoprval 4022  oprabval6g 4038  oprvalelrn 4045  caoprord2 4063  2ndconst 4103  elopabi 4123  eloprabi 4124  elrnoprabg 4130  oevn0 4160  om00el 4213  omordlim 4214  omlimcl 4215  ecopoprsym 4316  th3qlem1 4320  dom2d 4410  mapsnen 4435  undom 4444  xpdom2 4448  pw2en 4452  0sdomg 4472  fodomr 4489  mapdom2 4500  mapxpen 4501  xpmapenlem5 4506  unfilem1 4560  fodomfi 4575  fodomfiOLD 4576  inf3lem1 4622  r1tr 4664  rankval2 4680  rankr1 4684  rankval3 4691  unbndrank 4693  r1pwcl 4697  bnd2 4734  aceq0 4740  aceq5lem4 4748  aceq5 4750  axac 4755  ac6lem 4764  kmlem14 4788  iscard2 4865  alephord2 4887  cardaleph 4896  zfcndac 4983  ltexpi 5041  mulcmpblnq 5065  ordpipq 5068  ltsopq 5087  genpelv 5115  genpprecl 5116  genpnnp 5120  genpass 5124  distrlem1pr 5139  distrlem5pr 5143  prlem936a 5165  addcmpblnr 5193  ltsrpr 5198  ltsosr 5215  mulgt0sr 5226  map2psrpr 5232  ltresr 5270  axrnegex 5295  axrrecex 5296  pre-axltadd 5301  pre-axmulgt0 5302  negcon1t 5422  negcon2t 5423  xrrebndt 5580  lt0neg1t 5680  lt0neg2t 5681  le0neg1t 5682  le0neg2t 5683  divmul2t 5720  reclt1t 5900  recgt1t 5901  infm3 6056  arch 6073  supxrbnd 6093  nn0ltp1let 6129  elznn0 6151  elnnz1 6157  elnn0nn 6173  zltp1let 6183  recnzt 6193  dfuz 6204  uzindOLD 6210  uzwo3lem2 6219  seq1lem2 6311  iooint 6373  elioo1t 6379  elioo2t 6380  elioo3g 6381  elioc1t 6382  elico1t 6383  elicc1t 6384  elioo4g 6386  ioonegt 6407  iccnegt 6408  icounlem 6413  snunioolem 6415  ioojoint 6417  eluz1t 6421  raluz 6443  rexuz 6445  elfz1t 6471  elfz2t 6473  elfzuzb 6477  elfzuz2t 6487  elfz2nn0t 6496  fznn0t 6517  exple1t 6608  bernneq 6653  sqr2irrlem3 6727  crulem 6737  creur 6743  creui 6744  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 7488  acdc2 7491  acdc5 7494  acdc 7496  xpnnen 7500  infxpidmlem5 7557  infxpidmlem10 7562  isbasis2g 7611  isbasis3g 7612  eltg3t 7625  tgss3t 7637  elcls 7701  ntreq0 7705  islp 7741  islp2 7744  islpi 7746  cncnplem3 7773  cncnplem4 7774  ismet 7795  elbl 7835  blrn2 7839  blss 7850  metcnplem 7883  cncfmet 7902  dscmet 7915  lmbr2 7926  iscau2 7934  iscau5 7938  lmbrnns 7939  iscaunns 7941  metcn4 7968  isgrp 8038  issubg 8112  nvsubadd 8271  sspval 8378  isssp 8379  islno 8410  nmogtmnf 8429  nmounbi 8435  isblo 8438  ubthlem1 8525  spwmo 8652  pilem1 8666  sincosq1sgn 8699  sincosq2sgn 8700  efghgrpilem 8714  efif1lem5 8729  axgroth2 8773  grothinf 8776  hvmulcan2t 8935  hiret 8955  ocelt 9149  ocsh 9151  chocuni 9167  shselt 9273  shscomt 9278  shmods 9357  elspan 9461  adjsymt 9754  eigorth 9758  nmopgtmnf 9790  adjval2t 9810  cnvadj 9811  hhlno 9821  elnlfnt 9847  eleigvect 9876  nmop0h 9911  large 10189  mdbr2 10218  mddmd 10231  mdsl2 10244  chrelat3t 10293  atnem0 10299  irredlem1 10312  sumdmdi 10337  sumdmdlem 10340  dmdbr5at 10344  cdjreu 10354  elgiso 10393  uninqs 10436  elo 10439  cnfilca 10562  rcfpfillem3 10565  rcfpfillem6 10568  plimfilOLD 10580  eloi 10630  ishomc 10688  ismona 10708  ishgrag 10740

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