Theorem syl6bbr 597

Description: A syllogism inference from two biconditionals.

Hypotheses

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

Assertion

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

Proof of Theorem syl6bbr

Step	Hyp	Ref	Expression
1		syl6bbr.1	. 2 |- (ph -> (ps <-> ch))
2		syl6bbr.2	. . 3 |- (th <-> ch)
3	2	bicomi 189	. 2 |- (ch <-> th)
4	1, 3	syl6bb 595	1 |- (ph -> (ps <-> th))

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

This theorem is referenced by:  3bitr4g 614  biorf 807  equsal 1511  equsalOLD 1512  necon3bidOLD 2036  necon2abid 2065  eueq3 2430  sbc3angOLD 2509  sbcrext 2528  sbcrexgf 2530  sbcabel 2535  sbcel12g 2552  sbcel12gOLD 2553  sbceqdig 2554  sbceqdigOLD 2555  n0moeu 2887  reldisj 2916  r19.3rz 2960  r19.3rzv 2962  r19.9rzv 2963  dfiun2gOLD 3284  iununi 3331  iununiOLD 3332  otthg 3535  copsexgOLD 3538  sotrieqOLD 3617  ordelpss 3686  reuuni1OLD 3809  ordsucun 3905  onsucuni2OLD 3915  dflim3 3930  dfom2 3951  peano5 3975  iss 4254  elimasni 4292  eliniseg 4294  asymref2OLD 4311  xpcan 4348  xp11bOLD 4349  xpcan2 4350  xp11aOLD 4351  fcnvres 4589  dffn5 4717  fnrnfv 4718  funimass4 4722  eqfnfv2 4767  funimass3 4779  dff4 4791  fconst4 4827  elunirnALT 4845  eqfnoprv 4945  ordgt0ge1 5189  oelim2 5270  oaabs 5309  pw2en 5505  mapxpen 5589  r1pw 5797  rankonid 5806  sbc3org 5827  trsbc 5843  omsubsuc2 5878  aceq5lem4 5900  brdom6disj 5967  cardalephex 6034  indpi 6186  ltmpq 6229  distrlem5pr 6283  prlem934b 6290  suplem2pr 6314  letri3 6687  leltne 6691  ssxr 6714  xrleltne 6733  halfpos 7222  rpneg 7252  zrevaddcl 7379  elnnnn0 7381  znnsub 7386  znn0sub 7387  prime 7407  dfuzi 7414  qrevaddcl 7455  icounlem 7581  eluz2 7590  indstr 7630  fzsn 7684  fzpr 7685  om2uzf1oi 7712  lt2sqi 7869  le2sqi 7870  cau2i 8165  clm4fi 8342  clmnnsi 8344  clmfnn 8353  tgval3 8895  opnssneib 9005  islp2 9023  cldlp 9026  cncnplem3 9053  cncnplem4 9054  sncld 9064  metn0 9098  iscauf 9217  iscau5 9219  iscaunns 9222  caun0 9223  metcld 9245  nmolb 9773  nmlno0lem 9793  pilem3 10022  efif1lem1 10084  efif1lem2 10085  elghom 10195  hausfillim 10303  h2hcau 10481  h2hlm 10482  ocsh 10789  shle0 10999  eigrei 11397  nmoplb 11468  nmfnlb 11485  eleigvec2 11519  nmlnop0iALT 11557  jplem2 11841  cvbr2 11855  mdsl2bi 11895  chrelat3 11943  bnj112 12457  bnj117 12461  bnj921 12828  bnj919 12829  bnj971 12860  bnj123 13233  bnj218 13250  bnj578 13291  bnj607 13304  bnj873 13317  bnj1171 13439  bnj1283 13476  bnj1390 13513  elfzm11 13604  fz1eqblem 13608  algcvgblem 13745  dvdsgcd 13765  isprm2lem 13774  isprm3 13776  fundmpss 13836  dfon2 13858  tfrALTlem 13976  axfelem15 14045  r19.3rzvb 14273  unpde2eg2 14406  iint 15012  letri31 15019  algi 15074  rdmob 15095  btmp 15252  isplibg 15319  ccid 15363  elfiun 15369  inficlALT 15372  omsubsuc2OLD 15387  hscptsscld 15434  alexsub 15441  limfilcf 15587  fcluscf 15612  flimfnfcls 15615  inpreima 15682  inficl 15757  iccsplit 15854  heiborlem1 15955  divrngidl 16176  isdmn2 16203  prter1 16282  prtex 16284  prter3 16286  sbcnel12g 16408  sbcne12g 16409  pleval2 16785  hlrelat5 17050  isdivrngNEW 17160  paddvaln0 17262  paddval0 17271

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 164  df-an 242

Copyright terms: Public domain