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-1 5  ax-2 6  ax-3 7  ax-mp 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  2463  necon3abid  2549  necon3bid  2551  necon1abid  2569  r19.21t  2699  ceqsralt  2882  ceqsrexv  2972  ceqsrex2v  2974  elab2g  2987  elrabf  2993  eueq2  3010  eqreu  3028  reu8  3032  ru  3045  sbcralt  3118  sbcabel  3123  csbnestgf  3184  elcomplg  3218  disjpss  3601  ralprg  3775  rexprg  3776  difsn  3845  ralunsn  3879  dfiin2g  4000  iunxsng  4044  elpwuni  4053  eluni1g  4172  opkelopkabg  4245  otkelins2kg  4253  otkelins3kg  4254  opkelcokg  4261  opkelimagekg  4271  nnsucelrlem2  4425  ltfinirr  4457  sfin01  4528  addccan1  4560  copsex4g  4610  opelopabt  4699  opelopabga  4700  brabga  4701  dfid3  4768  opeliunxp  4820  resieq  4979  fncnv  5158  fununi  5160  fnssresb  5195  dffn5  5363  funimass4  5368  fniniseg  5371  fnsnfv  5373  dmfco  5381  fvimacnvi  5402  unpreima  5408  respreima  5410  dffo4  5423  fressnfv  5439  funiunfv  5467  dff13  5471  isomin  5496  isoini  5497  f1oiso  5499  fnopovb  5557  eloprabga  5578  resoprab2  5582  ov  5595  ovg  5601  fmpt2x  5730  txpcofun  5803  brcrossg  5848  mapsn  6026  enprmaplem5  6080  nenpw1pwlem2  6085  brltc  6114  elnc  6125  ncdisjun  6136  ce0nulnc  6184  ltlenlec  6207  ncfin  6247  nnc3n3p1  6278  fnfreclem3  6319