Theorem syl5bb 191

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 187	1 ⊢ (𝜒 → (𝜑 ↔ 𝜃))

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:  syl5rbb  192  syl5bbr  193  3bitr4g  222  imim21b  251  pm5.17dc  872  dn1dc  927  bilukdc  1357  nf4dc  1631  sbal1  1953  abbi  2228  necon3abid  2321  necon3bid  2323  necon1abiidc  2342  r19.21t  2481  ceqsralt  2684  ceqsrexv  2785  ceqsrex2v  2787  elab2g  2800  elrabf  2807  eueq2dc  2826  euxfrdc  2839  eqreu  2845  reu8  2849  ru  2877  sbcralt  2953  sbcrext  2954  sbcne12g  2987  csbnestgf  3018  dfss4st  3275  rexsng  3531  ralprg  3540  rexprg  3541  difsn  3623  opthpr  3665  ralunsn  3690  dfiin2g  3812  iunxsng  3854  iunxsngf  3856  elpwuni  3868  pwnss  4043  exmid01  4081  opelopabt  4144  opelopabga  4145  brabga  4146  elsucg  4286  elsuc2g  4287  brab2a  4552  opeliunxp  4554  posng  4571  brab2ga  4574  csbdmg  4693  elrnmpt1  4750  elrnmptg  4751  poleloe  4896  elxp4  4984  elxp5  4985  cnvpom  5039  sbcfung  5105  dffun8  5109  fncnv  5147  fununi  5149  fnssresb  5193  fnimaeq0  5202  funcocnv2  5348  dffn5im  5421  funimass4  5426  fnsnfv  5434  dmfco  5443  fndmdif  5479  fndmin  5481  unpreima  5499  respreima  5502  fsn2  5548  fnressn  5560  fressnfv  5561  elunirn  5621  dff13  5623  fliftel  5648  isoini  5673  f1oiso  5681  acexmid  5727  eloprabga  5812  resoprab2  5822  ralrnmpo  5839  rexrnmpo  5840  ovid  5841  ov  5844  ovg  5863  ofrfval2  5952  fmpox  6052  1stconst  6072  2ndconst  6073  f1od2  6086  rbropapd  6093  brtpos2  6102  dfsmo2  6138  frecabcl  6250  brdifun  6410  eqerlem  6414  brecop  6473  erovlem  6475  mapsn  6538  mptelixpg  6582  map1  6660  xpsnen  6668  xpdom2  6678  xpf1o  6691  supubti  6838  infglbti  6864  ctssdccl  6948  ltpiord  7075  nlt1pig  7097  elinp  7230  ltdfpr  7262  genpassl  7280  genpassu  7281  1idprl  7346  1idpru  7347  gt0srpr  7491  peano2nnnn  7588  recidpirq  7593  axprecex  7615  xrlenlt  7753  addsubeq4  7900  renegcl  7946  lesub0  8160  recexaplem2  8326  conjmulap  8402  rerecclap  8403  creui  8628  peano2nn  8642  nndiv  8671  elznn0  8973  eqreznegel  9308  ltxr  9455  divelunit  9678  iccf1o  9680  elfz2  9690  elfzp1  9745  fzdifsuc  9754  fznn  9762  fzosplitsni  9905  fvinim0ffz  9911  frec2uzisod  10073  sq11i  10275  cjreb  10531  rexfiuz  10653  cau3lem  10778  pwm1geoserap1  11169  mertensabs  11198  divides  11343  dvdsabseq  11393  odd2np1  11418  oddm1even  11420  modremain  11474  infssuzex  11490  bezoutlemnewy  11530  bezoutlemstep  11531  bezoutlemmain  11532  bezoutlema  11533  bezoutlemb  11534  isprm2  11644  isprm4  11646  dvdsnprmd  11652  istopg  12009  basgen2  12093  isnei  12156  restdis  12196  iscn  12208  iscnp  12210  lmbr2  12225  lmbrf  12226  txcn  12286  cnmpt21  12302  blres  12423  isxms2  12441  metrest  12495  metcnp  12501  txmetcnp  12507  txmetcn  12508  cnblcld  12524  bj-indeq  12817  bj-nn0sucALT  12866