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-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  bitr2id  192  bitr3id  193  3bitr4g  222  imim21b  251  pm5.17dc  899  dn1dc  955  bilukdc  1391  nf4dc  1663  sbal1  1995  abbi  2284  necon3abid  2379  necon3bid  2381  necon1abiidc  2400  r19.21t  2545  ceqsralt  2757  ceqsrexv  2860  ceqsrex2v  2862  elab2g  2877  elrabf  2884  eueq2dc  2903  euxfrdc  2916  eqreu  2922  reu8  2926  ru  2954  sbcralt  3031  sbcrext  3032  sbcne12g  3067  csbnestgf  3101  dfss4st  3360  rexsng  3622  ralprg  3632  rexprg  3633  difsn  3715  opthpr  3757  ralunsn  3782  dfiin2g  3904  iunxsng  3946  iunxsngf  3948  elpwuni  3960  pwnss  4143  exmid01  4182  opelopabt  4245  opelopabga  4246  brabga  4247  elsucg  4387  elsuc2g  4388  brab2a  4662  opeliunxp  4664  posng  4681  brab2ga  4684  csbdmg  4803  elrnmpt1  4860  elrnmptg  4861  poleloe  5008  elxp4  5096  elxp5  5097  cnvpom  5151  sbcfung  5220  dffun8  5224  fncnv  5262  fununi  5264  fnssresb  5308  fnimaeq0  5317  funcocnv2  5465  dffn5im  5540  funimass4  5545  fnsnfv  5553  dmfco  5562  fndmdif  5598  fndmin  5600  unpreima  5618  respreima  5621  fsn2  5667  fnressn  5679  fressnfv  5680  elunirn  5742  dff13  5744  fliftel  5769  isoini  5794  f1oiso  5802  acexmid  5849  eloprabga  5937  resoprab2  5947  ralrnmpo  5964  rexrnmpo  5965  ovid  5966  ov  5969  ovg  5988  ofrfval2  6074  fmpox  6176  1stconst  6197  2ndconst  6198  f1od2  6211  rbropapd  6218  brtpos2  6227  dfsmo2  6263  frecabcl  6375  brdifun  6536  eqerlem  6540  brecop  6599  erovlem  6601  mapsn  6664  mptelixpg  6708  map1  6786  xpsnen  6795  xpdom2  6805  xpf1o  6818  supubti  6972  infglbti  6998  ctssdccl  7084  ltpiord  7268  nlt1pig  7290  elinp  7423  ltdfpr  7455  genpassl  7473  genpassu  7474  1idprl  7539  1idpru  7540  gt0srpr  7697  mappsrprg  7753  map2psrprg  7754  peano2nnnn  7802  recidpirq  7807  axprecex  7829  xrlenlt  7971  addsubeq4  8121  renegcl  8167  lesub0  8385  recexaplem2  8557  conjmulap  8633  rerecclap  8634  creui  8863  peano2nn  8877  nndiv  8906  elznn0  9214  eqreznegel  9560  negelrp  9631  ltxr  9719  divelunit  9946  iccf1o  9948  elfz2  9959  elfzp1  10015  fzdifsuc  10024  fznn  10032  fzosplitsni  10178  fvinim0ffz  10184  frec2uzisod  10350  sq11i  10552  cjreb  10817  rexfiuz  10940  cau3lem  11065  pwm1geoserap1  11458  mertensabs  11487  divides  11738  dvdsabseq  11794  odd2np1  11819  oddm1even  11821  modremain  11875  infssuzex  11891  zsupssdc  11896  bezoutlemnewy  11938  bezoutlemstep  11939  bezoutlemmain  11940  bezoutlema  11941  bezoutlemb  11942  isprm2  12058  isprm4  12060  dvdsnprmd  12066  oddprmdvds  12293  4sqlem2  12328  issubm  12682  istopg  12750  basgen2  12834  isnei  12897  restdis  12937  iscn  12950  iscnp  12952  lmbr2  12967  lmbrf  12968  txcn  13028  cnmpt21  13044  blres  13187  isxms2  13205  metrest  13259  metcnp  13265  txmetcnp  13271  txmetcn  13272  cnblcld  13288  reopnap  13291  ioocosf1o  13528  bj-nn0sucALT  13973  apdiff  14040