Theorem syl6bb 535

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

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

This theorem is referenced by:  syl6rbb 536  syl6bbr 537  3bitr3g 553  biantrurd 726  19.17 1047  19.33b 1090  2eu6 1452  abeq2d 1569  necon2bbid 1620  eqvinc 1879  eueq3 1915  reu7 1931  reu8 1932  sbcralt 1986  sbcralgf 1988  uniiunlem 2128  reldisj 2309  eqsn 2470  eluniab 2508  elintab 2539  dfiun2g 2581  axsep2 2699  notzfaus 2736  sbcsng 2748  moabex 2761  opeqsn 2797  sotrieq2 2857  reuxfr 2899  elpwunsn 2907  ordtri2 2977  ordtri4 2979  oneqmini 3012  ordtri2or 3072  ralxp 3213  relop 3270  opelcog 3285  opelcnvg 3291  dmsnop 3323  reldm0 3326  relrn0 3350  iss 3389  asymref2 3432  xpnz 3458  fncnv 3553  fvprc 3712  fnopfvb 3745  funopfvb 3747  fvelrnb 3751  funimass4 3754  fvopab3 3768  fvopabn 3777  eqfnfvf 3789  elrnopabg 3791  fsn 3825  fconstfv 3840  funiunfv 3857  f1fv 3865  f1ocnvfv3 3874  isocnv 3887  isoini 3891  f1oiso 3895  eloprabg 3998  resoprab 4000  eqfnoprval 4007  oprabval6g 4023  oprvalelrn 4030  caoprord2 4049  2ndconst 4087  elopabi 4107  eloprabi 4108  elrnoprabg 4114  oevn0 4144  om00el 4197  omordlim 4198  omlimcl 4199  ecopoprsym 4300  th3qlem1 4304  dom2d 4391  mapsnen 4416  undom 4424  xpdom2 4428  pw2en 4432  0sdomg 4452  fodomr 4469  mapdom2 4480  mapxpen 4481  xpmapenlem5 4486  unfilem1 4530  abfii4 4544  fodomfi 4546  inf3lem1 4593  r1tr 4634  rankval2 4650  rankr1 4654  rankval3 4661  unbndrank 4663  r1pwcl 4667  bnd2 4704  aceq0 4710  aceq5lem4 4718  aceq5 4720  axac 4725  ac6lem 4734  kmlem14 4758  iscard2 4834  alephord2 4856  cardaleph 4865  zfcndac 4951  ltexpi 5009  mulcmpblnq 5033  ordpipq 5036  ltsopq 5055  genpelv 5083  genpprecl 5084  genpnnp 5088  genpass 5092  distrlem1pr 5107  distrlem5pr 5111  prlem936a 5133  addcmpblnr 5161  ltsrpr 5166  ltsosr 5183  mulgt0sr 5194  map2psrpr 5200  ltresr 5238  axrnegex 5263  axrrecex 5264  pre-axltadd 5269  pre-axmulgt0 5270  negcon1t 5390  negcon2t 5391  xrrebndt 5549  lt0neg1t 5649  lt0neg2t 5650  le0neg1t 5651  le0neg2t 5652  divmul2t 5685  reclt1t 5854  recgt1t 5855  infm3 6009  arch 6026  supxrbnd 6046  nn0ltp1let 6082  elznn0 6104  elnnz1 6110  elnn0nn 6126  zltp1let 6136  recnzt 6146  dfuz 6158  uzindOLD 6164  uzwo3lem2 6173  seq1lem2 6255  iooint 6317  elioo1t 6323  elioo2t 6324  elioo3g 6325  elioo4g 6326  elioc1t 6327  elico1t 6328  elicc1t 6329  ioonegt 6347  iccnegt 6348  icounlem 6353  snunioolem 6355  eluz1t 6360  raluz 6382  rexuz 6384  elfz1t 6410  elfz2t 6412  elfzuzb 6416  elfzuz2t 6426  elfz2nn0t 6435  fznn0t 6456  exple1t 6546  bernneq 6591  sqr2irrlem3 6664  crulem 6674  creur 6681  creui 6682  abssubne0t 6828  cvg2 6867  dffsum 6944  fsumrev 6975  fsumshft 6977  clm1 7023  clmnns 7030  climshft 7049  climres 7050  caucvg 7107  caucvg3t 7112  dfisum 7135  acdc3 7437  acdc2 7440  acdc5 7443  acdc 7445  xpnnen 7449  infxpidmlem5 7507  infxpidmlem10 7512  istop2g 7547  isbasis2g 7562  isbasis3g 7563  eltg3t 7576  tgss3t 7588  elcls 7654  ntreq0 7658  islp 7694  islp2 7697  islpi 7699  cncnplem3 7726  cncnplem4 7727  ismet 7748  elbl 7790  blrn2 7794  blss 7805  metcnplem 7838  cncfmet 7857  dscmet 7870  lmbr2 7881  iscau2 7889  iscau5 7893  lmbrnns 7894  metcn4 7921  isgrp 7991  issubg 8068  nvsubadd 8227  sspval 8329  isssp 8330  islno 8361  nmogtmnf 8378  nmounbi 8384  isblo 8387  ubthlem1 8473  spwmo 8598  pilem1 8609  sincosq1sgn 8640  sincosq2sgn 8641  efghgrpilem 8653  efif1lem5 8668  axgroth2 8717  grothinf 8720  hvmulcan2t 8879  hiret 8899  ocelt 9093  ocsh 9095  chocuni 9111  shselt 9216  shscomt 9221  shmods 9300  elspan 9404  adjsymt 9699  eigorth 9703  nmopgtmnf 9735  adjval2t 9755  cnvadj 9756  hhlno 9766  elnlfnt 9791  eleigvect 9820  nmop0h 9854  large 10132  mdbr2 10161  mddmd 10173  mdsl2 10186  chrelat3t 10235  atnem0 10241  irredlem1 10254  sumdmdi 10278  sumdmdlem 10281  dmdbr5at 10284  cdjreu 10293  elgiso 10332  uninqs 10378  elo 10381  cnfilca 10487  eloi 10539  ishomc 10597  ismona 10615  ishgrag 10641

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