Theorem syl5bb 248

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

Hypotheses

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

Assertion

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

Proof of Theorem syl5bb

Step	Hyp	Ref	Expression
1		syl5bb.1	. . 3 |- (ph <-> ps)
2	1	a1i 10	. 2 |- (ch -> (ph <-> ps))
3		syl5bb.2	. 2 |- (ch -> (ps <-> th))
4	2, 3	bitrd 244	1 |- (ch -> (ph <-> th))

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

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 177

This theorem is referenced by:  syl5rbb  249  syl5bbr  250  3bitr4g  279  imim21b  356  cad0  1400  had1  1402  ax11wdemo  1723  ax12olem6  1932  sbcom  2089  abbi  2464  necon3abid  2550  necon3bid  2552  necon1abid  2570  r19.21t  2700  ceqsralt  2883  ceqsrexv  2973  ceqsrex2v  2975  elab2g  2988  elrabf  2994  eueq2  3011  eqreu  3029  reu8  3033  ru  3046  sbcralt  3119  sbcabel  3124  csbnestgf  3185  elcomplg  3219  disjpss  3602  ralprg  3776  rexprg  3777  difsn  3846  ralunsn  3880  dfiin2g  4001  iunxsng  4045  elpwuni  4054  eluni1g  4173  opkelopkabg  4246  otkelins2kg  4254  otkelins3kg  4255  opkelcokg  4262  opkelimagekg  4272  nnsucelrlem2  4426  ltfinirr  4458  sfin01  4529  addccan1  4561  copsex4g  4611  opelopabt  4700  opelopabga  4701  brabga  4702  dfid3  4769  opeliunxp  4821  resieq  4980  fncnv  5159  fununi  5161  fnssresb  5196  dffn5  5364  funimass4  5369  fniniseg  5372  fnsnfv  5374  dmfco  5382  fvimacnvi  5403  unpreima  5409  respreima  5411  dffo4  5424  fressnfv  5440  funiunfv  5468  dff13  5472  isomin  5497  isoini  5498  f1oiso  5500  fnopovb  5558  eloprabga  5579  resoprab2  5583  ov  5596  ovg  5602  fmpt2x  5731  txpcofun  5804  brcrossg  5849  mapsn  6027  enprmaplem5  6081  nenpw1pwlem2  6086  brltc  6115  elnc  6126  ncdisjun  6137  ce0nulnc  6185  ltlenlec  6208  ncfin  6248  nnc3n3p1  6279  fnfreclem3  6320