Theorem syl6bbr 197

Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)

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

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3bitr4g  222  bibi2i  226  equsalh  1668  eueq3dc  2803  sbcel12g  2960  sbceqg  2961  sbcnel12g  2962  reldisj  3353  r19.3rm  3390  rabxp  4504  elrng  4658  iss  4791  eliniseg  4835  fcnvres  5229  dffv3g  5336  funimass4  5390  fndmdif  5443  fneqeql  5446  funimass3  5454  elrnrexdmb  5478  dff4im  5484  fconst4m  5556  elunirn  5583  riota1  5664  riota2df  5666  f1ocnvfv3  5679  eqfnov  5789  caoftrn  5918  mpt2xopovel  6044  rntpos  6060  ordgt0ge1  6237  iinerm  6404  erinxp  6406  qliftfun  6414  mapdm0  6460  isomnimap  6880  ismkvmap  6898  pr2nelem  6916  indpi  6998  genpdflem  7163  genpdisj  7179  genpassl  7180  genpassu  7181  ltnqpri  7250  ltpopr  7251  ltexprlemm  7256  ltexprlemdisj  7262  ltexprlemloc  7263  ltrennb  7488  letri3  7663  letr  7665  ltneg  8037  leneg  8040  reapltxor  8163  apsym  8180  suprnubex  8511  suprleubex  8512  elnnnn0  8814  zrevaddcl  8898  znnsub  8899  znn0sub  8913  prime  8944  eluz2  9124  eluz2b1  9187  nn01to3  9201  qrevaddcl  9228  xrletri3  9371  xrletr  9374  iccid  9491  elicopnf  9535  fzsplit2  9613  fzsn  9629  fzpr  9640  uzsplit  9655  fvinim0ffz  9801  lt2sqi  10157  le2sqi  10158  abs00ap  10610  iooinsup  10820  mertenslem2  11079  gcddiv  11435  algcvgblem  11458  isprm3  11527  eltg2b  11906  discld  11988  opnssneib  12008  restbasg  12020  ssidcn  12061  cnptoprest2  12091  lmss  12097  bldisj  12187  xmeter  12222  bl2ioo  12316  bj-sseq  12400  nnti  12597