Theorem syl6bbr 538

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

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

This theorem is referenced by:  3bitr4g 555  biorf 735  equsal 1151  necon3bid 1601  necon2abid 1622  eueq3 1919  sbc3ang 1979  sbcrext 1991  sbcrexgf 1993  sbcabel 1996  sbcel12g 2011  sbceqdig 2012  r19.3rzv 2348  r19.9rzv 2349  dfiun2g 2586  iununi 2616  otthg 2790  copsexg 2792  sotrieq 2861  reuuni1 2882  ordelpss 2975  ordsucun 3082  onsucuni2 3091  dfom2 3133  peano5 3153  asymref2 3440  xp11a 3477  xp11b 3478  fcnvres 3648  fnopabfv 3758  fnrnfv 3759  funimass4 3763  fvreseq 3799  funimass3 3806  dff3 3818  fconst4 3851  elunirnALT 3869  eqfnoprval 4016  ordgt0ge1 4144  oelim2 4222  oaabs 4252  pw2en 4446  mapenlem2 4490  mapxpen 4495  r1pw 4686  rankonid 4695  aceq5lem4 4738  brdom6disj 4805  cardalephex 4886  indpi 5034  ltmpq 5077  distrlem5pr 5131  prlem934b 5138  suplem2pr 5162  letri3t 5517  leltnet 5521  xrleltnet 5558  halfpost 6036  zrevaddclt 6170  elnnnn0 6172  znnsubt 6177  znn0subt 6178  primet 6195  dfuz 6202  qrevaddclt 6275  om2uzf1o 6301  icounlem 6412  eluz2t 6421  indstr 6461  lt2sq 6624  le2sq 6625  cau2 6913  clm4f 7082  clmnns 7084  clmfnn 7093  ser1f0 7170  tgval3t 7625  opnssneib 7729  islp2 7747  cldlp 7750  cncnplem3 7776  cncnplem4 7777  sncld 7787  metne0 7821  iscauf 7939  iscau5 7941  iscaunns 7944  caun0 7945  metcld 7967  nmolb 8434  nmlno0lem 8453  phoeqi 8518  pilem3 8673  efif1lem1 8730  efif1lem2 8731  h2hcau 8849  h2hlm 8850  ocsh 9156  shle0t 9366  hoeq1t 9756  eigre 9760  nmoplbt 9831  nmfnlbt 9848  eleigvec2t 9882  nmlnop0ALT 9920  jplem2 10196  cvbr2t 10210  mdsl2b 10250  chrelat3t 10298  elghom 10384  r19.3rzvb 10437  unpde2eg2 10544  iint 10634  algi 10660  rdmob 10681

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