Theorem syl5bbr 274

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

Hypotheses

Ref	Expression
syl5bbr.1	|- ( ps <-> ph )
syl5bbr.2	|- ( ch -> ( ps <-> th ) )

Assertion

Ref	Expression
syl5bbr	|- ( ch -> ( ph <-> th ) )

Proof of Theorem syl5bbr

Step	Hyp	Ref	Expression
1		syl5bbr.1	. . 3 |- ( ps <-> ph )
2	1	bicomi 214	. 2 |- ( ph <-> ps )
3		syl5bbr.2	. 2 |- ( ch -> ( ps <-> th ) )
4	2, 3	syl5bb 272	1 |- ( ch -> ( ph <-> th ) )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197

This theorem is referenced by:  3bitr3g  302  biass  374  19.16  2093  19.19  2097  sbcom2  2445  sbal2  2461  necon1bbid  2833  rspc2gv  3321  elabgt  3347  sbceq1a  3446  sbcralt  3510  sbccsb2  4005  disjxun  4651  dfres3  5403  xp11  5569  ressn  5671  fnssresb  6003  dmfco  6272  dffo4  6375  f1ompt  6382  funressn  6426  elunirnALT  6510  fliftf  6565  resoprab2  6757  elrnmpt2res  6774  ralrnmpt2  6775  iunpw  6978  ordunisuc2  7044  tfis  7054  tfinds  7059  dfom2  7067  fun11iun  7126  opiota  7229  1stconst  7265  2ndconst  7266  fnsuppeq0  7323  iinon  7437  dfsmo2  7444  oeeui  7682  omabs  7727  brecop  7840  ixpsnf1o  7948  boxcutc  7951  ac6sfi  8204  wemapwe  8594  sdom2en01  9124  ac6num  9301  zorn2lem7  9324  ttukeylem6  9336  alephval2  9394  fpwwe2  9465  fpwwe  9468  nqereu  9751  suplem2pr  9875  map2psrpr  9931  supsrlem  9932  fimaxre3  10970  infm3  10982  crne0  11013  nn1suc  11041  xmulneg1  12099  supxrbnd1  12151  supxrbnd2  12152  iccneg  12293  wrdmap  13336  wrdind  13476  rtrclreclem3  13800  cnpart  13980  sqrt00  14004  lo1resb  14295  o1resb  14297  absefib  14928  efieq1re  14929  sadadd2lem2  15172  saddisjlem  15186  prmind2  15398  isprm7  15420  mreacs  16319  issubc  16495  isfunc  16524  pospo  16973  mrcmndind  17366  eqgval  17643  resscntz  17764  frgpuplem  18185  qusabl  18268  dmdprd  18397  dprdcntz2  18437  dprd2d2  18443  isnzr2  19263  mpfind  19536  gsummoncoe1  19674  pf1ind  19719  chrdvds  19876  chrcong  19877  znleval  19903  isphld  19999  smadiadetr  20481  mp2pm2mplem4  20614  isclo  20891  ist1-2  21151  isnrm2  21162  bwth  21213  nconnsubb  21226  subislly  21284  ptclsg  21418  qtopcld  21516  kqcldsat  21536  qustgplem  21924  tsmssubm  21946  ustuqtop  22050  utop2nei  22054  blval2  22367  caucfil  23081  ioorinv  23344  mbfss  23413  iblss2  23572  dvivthlem1  23771  lhop1  23777  deg1leb  23855  reeff1o  24201  sincosq3sgn  24252  sincosq4sgn  24253  dcubic  24573  efrlim  24696  fsumharmonic  24738  isppw  24840  issqf  24862  fsumdvdsmul  24921  ppiub  24929  lgsdinn0  25070  tglngne  25445  tgelrnln  25525  axlowdimlem14  25835  nbgrssovtx  26260  eupth2lem2  27079  fusgr2wsp2nb  27198  h2hlm  27837  isch2  28080  ch0pss  28304  nmcfnlbi  28911  jplem1  29127  hatomistici  29221  mdsymlem5  29266  cdjreui  29291  reuxfr4d  29330  dfimafnf  29436  funcnvmpt  29468  fpwrelmap  29508  nn0min  29567  isarchi  29736  ordtconnlem1  29970  esumfsup  30132  esumpcvgval  30140  measvuni  30277  aean  30307  eulerpartlemgh  30440  ballotlemsima  30577  sgn3da  30603  bnj1468  30916  subfacp1lem2a  31162  subfacp1lem6  31167  eldm3  31651  onsuct0  32440  bj-restsn  33035  ptrest  33408  ptrecube  33409  poimirlem2  33411  poimirlem23  33432  sdclem2  33538  fdc  33541  fdc1  33542  istotbnd3  33570  sstotbnd  33574  prdstotbnd  33593  rrncmslem  33631  brinxprnres  34059  alrmomo2  34124  lub0N  34476  glb0N  34480  cdlemefrs29bpre0  35684  dvhb1dimN  36274  dvhopellsm  36406  dibord  36448  dochnel2  36681  mapdvalc  36918  mapdval4N  36921  diophin  37336  diophun  37337  diophrex  37339  3rexfrabdioph  37361  6rexfrabdioph  37363  7rexfrabdioph  37364  zindbi  37511  rababg  37879  relexpnul  37970  clsk1independent  38344  hashnzfzclim  38521  fveqsb  38657  infxrbnd2  39585  cncfiooicclem1  40106  stoweidlem35  40252  tz6.12-afv  41253  ndmaovg  41264  aacllem  42547