Theorem syl6bbr 536

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

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

This theorem is referenced by:  3bitr4g 553  biorf 733  equsal 1147  necon3bid 1593  necon2abid 1614  eueq3 1910  sbc3ang 1969  sbcrext 1981  sbcrexgf 1983  sbcabel 1986  sbcel12g 2001  sbceqdig 2002  r19.3rzv 2338  r19.9rzv 2339  dfiun2g 2576  iununi 2606  otthg 2780  copsexg 2782  sotrieq 2852  reuuni1 2872  ordelpss 2965  ordsucun 3072  onsucuni2 3081  dfom2 3123  peano5 3143  asymref2 3424  asymref2OLD 3426  xp11a 3464  fcnvres 3633  fnopabfv 3743  fnrnfv 3744  funimass4 3748  fvreseq 3784  funimass3 3791  dff3 3803  fconst4 3836  elunirnALT 3854  eqfnoprval 4001  ordgt0ge1 4128  oelim2 4206  oaabs 4236  pw2en 4426  mapenlem2 4470  mapxpen 4475  r1pw 4658  rankonid 4667  aceq5lem4 4710  brdom6disj 4777  cardalephex 4858  indpi 5006  ltmpq 5049  distrlem5pr 5103  prlem934b 5110  suplem2pr 5134  letri3t 5490  leltnet 5494  xrleltnet 5531  halfpost 5983  zrevaddclt 6117  elnnnn0 6119  znnsubt 6124  znn0subt 6125  primet 6142  dfuz 6150  qrevaddclt 6213  om2uzf1o 6238  icounlem 6345  eluz2t 6353  indstr 6393  lt2sq 6555  le2sq 6556  cau2 6850  clm4f 7020  clmnns 7022  ser1f0 7106  znnen 7445  tgval3t 7567  opnssneib 7670  islp2 7688  cncnplem3 7715  cncnplem4 7716  sncld 7726  iscauf 7877  iscau5 7878  caun0 7880  metcld 7901  nmolb 8366  nmlno0lem 8385  phoeqi 8449  pilem3 8592  efif1lem1 8645  efif1lem2 8646  h2hcau 8788  h2hlm 8789  ocsh 9072  shle0t 9281  hoeq1t 9673  eigre 9677  nmoplbt 9748  nmfnlbt 9764  eleigvec2t 9798  nmlnop0ALT 9835  jplem2 10106  cvbr2t 10120  mdsl2b 10158  chrelat3t 10206  elghom 10289  r19.3rzvb 10337  iint 10478  algi 10504  rdmob 10525

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