Theorem syl5bb 181

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

Hypotheses

Ref	Expression
syl5bb.1	⊢ (𝜑 ↔ 𝜓)
syl5bb.2	⊢ (𝜒 → (𝜓 ↔ 𝜃))

Assertion

Ref	Expression
syl5bb	⊢ (𝜒 → (𝜑 ↔ 𝜃))

Proof of Theorem syl5bb

Step	Hyp	Ref	Expression
1		syl5bb.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	a1i 9	. 2 ⊢ (𝜒 → (𝜑 ↔ 𝜓))
3		syl5bb.2	. 2 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
4	2, 3	bitrd 177	1 ⊢ (𝜒 → (𝜑 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  syl5rbb  182  syl5bbr  183  3bitr4g  212  imim21b  241  pm5.17dc  810  dn1dc  867  bilukdc  1287  nf4dc  1560  sbal1  1878  abbi  2151  necon3abid  2244  necon3bid  2246  necon1abiidc  2265  r19.21t  2394  ceqsralt  2581  ceqsrexv  2674  ceqsrex2v  2676  elab2g  2689  elrabf  2696  eueq2dc  2714  euxfrdc  2727  eqreu  2733  reu8  2737  ru  2763  sbcralt  2834  sbcrext  2835  sbcne12g  2868  csbnestgf  2898  disjpss  3278  ralprg  3421  rexprg  3422  difsn  3501  opthpr  3543  ralunsn  3568  dfiin2g  3690  iunxsng  3732  elpwuni  3741  pwnss  3912  opelopabt  3999  opelopabga  4000  brabga  4001  elsucg  4141  elsuc2g  4142  brab2a  4393  opeliunxp  4395  posng  4412  brab2ga  4415  csbdmg  4529  elrnmpt1  4585  elrnmptg  4586  poleloe  4724  elxp4  4808  elxp5  4809  cnvpom  4860  sbcfung  4925  dffun8  4929  fncnv  4965  fununi  4967  fnssresb  5011  fnimaeq0  5020  funcocnv2  5151  dffn5im  5219  funimass4  5224  fnsnfv  5232  dmfco  5241  fndmdif  5272  fndmin  5274  unpreima  5292  respreima  5295  fsn2  5337  fnressn  5349  fressnfv  5350  elunirn  5405  dff13  5407  fliftel  5433  isoini  5457  f1oiso  5465  acexmid  5511  eloprabga  5591  resoprab2  5598  ralrnmpt2  5615  rexrnmpt2  5616  ovid  5617  ov  5620  ovg  5639  ofrfval2  5727  fmpt2x  5826  1stconst  5842  2ndconst  5843  isprmpt2  5858  brtpos2  5866  dfsmo2  5902  brdifun  6133  eqerlem  6137  brecop  6196  erovlem  6198  xpsnen  6295  xpdom2  6305  ltpiord  6417  nlt1pig  6439  elinp  6572  ltdfpr  6604  genpassl  6622  genpassu  6623  1idprl  6688  1idpru  6689  gt0srpr  6833  peano2nnnn  6929  recidpirq  6934  axprecex  6954  xrlenlt  7084  addsubeq4  7226  renegcl  7272  lesub0  7474  recexaplem2  7633  conjmulap  7705  rerecclap  7706  creui  7912  peano2nn  7926  nndiv  7954  elznn0  8260  eqreznegel  8549  ltxr  8695  divelunit  8870  iccf1o  8872  elfz2  8881  elfzp1  8934  fzdifsuc  8943  fznn  8951  fzosplitsni  9091  fvinim0ffz  9096  frec2uzisod  9193  sq11i  9343  cjreb  9466  cau3lem  9710  bj-indeq  10053  bj-nn0sucALT  10103