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  3101  sbcnel12g  3158  elxp4  5255  elxp5  5256  f1eq123d  5611  foeq123d  5612  f1oeq123d  5613  fnmptfvd  5787  ofrfval  6284  eloprabi  6405  fnmpoovd  6424  suppsnopdc  6463  smoeq  6534  ecidg  6846  ixpsnval  6949  mapsnend  7065  enqbreq2  7688  ltanqg  7731  caucvgprprlemexb  8038  caucvgsrlemgt1  8126  caucvgsrlemoffres  8131  ltrennb  8185  apneg  8903  mulext1  8904  apdivmuld  9107  ltdiv23  9186  lediv23  9187  halfpos  9489  addltmul  9495  div4p1lem1div2  9512  ztri3or  9640  supminfex  9950  iccf1o  10360  fzsplit3  10410  fzshftral  10467  fzoshftral  10609  infssuzex  10618  2tnp1ge0ge0  10688  fihashen1  11190  seq3coll  11242  s111  11347  swrdspsleq  11387  pfxeq  11416  wrd2ind  11443  cjap  11619  negfi  11941  tanaddaplem  12452  dvdssub  12552  addmodlteqALT  12573  dvdsmod  12576  oddp1even  12590  nn0o1gt2  12619  nn0oddm1d2  12623  bitscmp  12672  cncongr1  12828  cncongr2  12829  4sqlem11  13127  4sqlem17  13133  ballotfilemsima  13206  intopsn  13633  sgrp1  13677  sgrppropd  13679  issubg  13929  nmzsubg  13966  conjnmzb  14036  rng1zrlem  14201  ring1  14305  issubrg  14470  znf1o  14928  znleval  14930  znunit  14936  elmopn  15440  metss  15488  comet  15493  xmetxp  15501  limcmpted  15657  cnlimc  15666  lgsneg  16026  lgsne0  16040  lgsprme0  16044  lgsquadlem1  16079  lgsquadlem2  16080  2lgs  16106  2lgsoddprm  16115  edg0iedg0g  16190  wrdupgren  16220  wrdumgren  16230  vtxd0nedgbfi  16423  eupth2lem2dc  16583  eupth2lem3lem6fi  16595  eupth2lem3lem4fi  16597