Theorem syl6bbr 541

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 170	. 2 |- (ch <-> th)
4	1, 3	syl6bb 539	1 |- (ph -> (ps <-> th))

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

This theorem is referenced by:  3bitr4g 558  biorf 740  equsal 1188  necon3bid 1644  necon2abid 1666  eueq3 1965  sbc3ang 2027  sbcrext 2041  sbcrexgf 2043  sbcabel 2046  sbcel12g 2062  sbceqdig 2063  r19.3rzv 2402  r19.9rzv 2403  dfiun2g 2654  iununi 2686  otthg 2866  copsexg 2868  sotrieq 2940  ordelpss 3003  reuuni1 3106  ordsucun 3180  onsucuni2 3188  dfom2 3220  peano5 3241  asymref2 3532  xp11a 3562  xp11b 3563  fcnvres 3755  dffn5 3869  fnrnfv 3870  funimass4 3874  funimass3 3920  dff4 3932  fconst4 3965  elunirnALT 3983  eqfnoprv 4076  ordgt0ge1 4280  oelim2 4358  oaabs 4392  pw2en 4587  mapxpen 4642  r1pw 4832  rankonid 4841  aceq5lem4 4884  brdom6disj 4951  cardalephex 5036  indpi 5188  ltmpq 5231  distrlem5pr 5285  prlem934b 5292  suplem2pr 5316  letri3 5671  leltne 5675  xrleltne 5712  halfpos 6182  rpneg 6211  zrevaddcl 6338  elnnnn0 6340  znnsub 6345  znn0sub 6346  prime 6366  dfuzi 6373  qrevaddcl 6414  icounlem 6539  eluz2 6548  indstr 6588  om2uzf1oi 6664  lt2sqi 6821  le2sqi 6822  cau2i 7116  clm4fi 7285  clmnnsi 7287  clmfnn 7296  tgval3 7837  opnssneib 7939  islp2 7957  cldlp 7960  cncnplem3 7986  cncnplem4 7987  sncld 7997  metn0 8031  iscauf 8150  iscau5 8152  iscaunns 8155  caun0 8156  metcld 8178  nmolb 8688  nmlno0lem 8708  pilem3 8940  efif1lem1 9002  efif1lem2 9003  h2hcau 9124  h2hlm 9125  ocsh 9432  shle0 9642  eigrei 10040  nmoplb 10111  nmfnlb 10128  eleigvec2 10162  nmlnop0iALT 10199  jplem2 10477  cvbr2 10491  mdsl2bi 10531  chrelat3 10579  elghom 10669  r19.3rzvb 10721  letri31 10791  unpde2eg2 10825  iint 11157  algi 11181  rdmob 11202  ccid 11412  elfiun 11421  inficlALT 11424  omsubsuc2 11439  hscptsscld 11491  alexsub 11500  limfilcf 11683  hausfillim 11685  fcluscf 11724  flimfnfcls 11727  inpreima 11793  inficl 11849  fzsn 11865  fzpr 11866  iccsplit 11919  heiborlem1 12011

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 145  df-an 223

Copyright terms: Public domain