Theorem 3bitrd 214

Description: Deduction from transitivity of biconditional. (Contributed by NM, 13-Aug-1999.)

Hypotheses

Ref	Expression
3bitrd.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
3bitrd.2	⊢ (𝜑 → (𝜒 ↔ 𝜃))
3bitrd.3	⊢ (𝜑 → (𝜃 ↔ 𝜏))

Assertion

Ref	Expression
3bitrd	⊢ (𝜑 → (𝜓 ↔ 𝜏))

Proof of Theorem 3bitrd

Step	Hyp	Ref	Expression
1		3bitrd.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		3bitrd.2	. . 3 ⊢ (𝜑 → (𝜒 ↔ 𝜃))
3	1, 2	bitrd 188	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4		3bitrd.3	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
5	3, 4	bitrd 188	1 ⊢ (𝜑 → (𝜓 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sbceqal  3098  sbcnel12g  3155  elxp4  5250  elxp5  5251  f1eq123d  5606  foeq123d  5607  f1oeq123d  5608  fnmptfvd  5782  ofrfval  6275  eloprabi  6392  fnmpoovd  6411  suppsnopdc  6450  smoeq  6521  ecidg  6833  ixpsnval  6936  mapsnend  7052  enqbreq2  7672  ltanqg  7715  caucvgprprlemexb  8022  caucvgsrlemgt1  8110  caucvgsrlemoffres  8115  ltrennb  8169  apneg  8885  mulext1  8886  apdivmuld  9087  ltdiv23  9166  lediv23  9167  halfpos  9469  addltmul  9475  div4p1lem1div2  9492  ztri3or  9620  supminfex  9929  iccf1o  10338  fzshftral  10442  fzoshftral  10584  infssuzex  10593  2tnp1ge0ge0  10661  fihashen1  11162  seq3coll  11214  s111  11319  swrdspsleq  11359  pfxeq  11388  wrd2ind  11415  cjap  11591  negfi  11913  tanaddaplem  12424  dvdssub  12524  addmodlteqALT  12545  dvdsmod  12548  oddp1even  12562  nn0o1gt2  12591  nn0oddm1d2  12595  bitscmp  12644  cncongr1  12800  cncongr2  12801  4sqlem11  13099  4sqlem17  13105  intopsn  13580  sgrp1  13624  sgrppropd  13626  issubg  13890  nmzsubg  13927  conjnmzb  13997  srg1zr  14131  ring1  14203  issubrg  14366  znf1o  14799  znleval  14801  znunit  14807  elmopn  15311  metss  15359  comet  15364  xmetxp  15372  limcmpted  15528  cnlimc  15537  lgsneg  15897  lgsne0  15911  lgsprme0  15915  lgsquadlem1  15950  lgsquadlem2  15951  2lgs  15977  2lgsoddprm  15986  edg0iedg0g  16061  wrdupgren  16091  wrdumgren  16101  vtxd0nedgbfi  16294  eupth2lem2dc  16454  eupth2lem3lem6fi  16466  eupth2lem3lem4fi  16468