Theorem syl6bbr 537

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

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

This theorem is referenced by:  3bitr4g 554  biorf 734  equsal 1150  necon3bid 1599  necon2abid 1620  eueq3 1916  sbc3ang 1976  sbcrext 1988  sbcrexgf 1990  sbcabel 1993  sbcel12g 2008  sbceqdig 2009  r19.3rzv 2345  r19.9rzv 2346  dfiun2g 2582  iununi 2612  otthg 2786  copsexg 2788  sotrieq 2857  reuuni1 2878  ordelpss 2971  ordsucun 3078  onsucuni2 3087  dfom2 3129  peano5 3149  asymref2 3436  xp11a 3473  xp11b 3474  fcnvres 3643  fnopabfv 3753  fnrnfv 3754  funimass4 3758  fvreseq 3794  funimass3 3801  dff3 3813  fconst4 3846  elunirnALT 3864  eqfnoprval 4011  ordgt0ge1 4137  oelim2 4215  oaabs 4245  pw2en 4435  mapenlem2 4479  mapxpen 4484  r1pw 4669  rankonid 4678  aceq5lem4 4721  brdom6disj 4788  cardalephex 4869  indpi 5017  ltmpq 5060  distrlem5pr 5114  prlem934b 5121  suplem2pr 5145  letri3t 5500  leltnet 5504  xrleltnet 5541  halfpost 5993  zrevaddclt 6127  elnnnn0 6129  znnsubt 6134  znn0subt 6135  primet 6152  dfuz 6160  qrevaddclt 6225  om2uzf1o 6251  icounlem 6358  eluz2t 6366  indstr 6406  lt2sq 6569  le2sq 6570  cau2 6865  clm4f 7035  clmnns 7037  clmfnn 7046  ser1f0 7123  znnen 7462  tgval3t 7585  opnssneib 7689  islp2 7707  cldlp 7710  cncnplem3 7736  cncnplem4 7737  sncld 7747  metne0 7783  iscauf 7901  iscau5 7903  iscaunns 7906  caun0 7907  metcld 7929  nmolb 8394  nmlno0lem 8413  phoeqi 8477  pilem3 8627  efif1lem1 8680  efif1lem2 8681  h2hcau 8804  h2hlm 8805  ocsh 9111  shle0t 9321  hoeq1t 9713  eigre 9717  nmoplbt 9788  nmfnlbt 9805  eleigvec2t 9839  nmlnop0ALT 9876  jplem2 10152  cvbr2t 10166  mdsl2b 10206  chrelat3t 10254  elghom 10340  r19.3rzvb 10395  iint 10550  algi 10576  rdmob 10597

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