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  3045  sbcnel12g  3101  elxp4  5158  elxp5  5159  f1eq123d  5499  foeq123d  5500  f1oeq123d  5501  fnmptfvd  5669  ofrfval  6148  eloprabi  6263  fnmpoovd  6282  smoeq  6357  ecidg  6667  ixpsnval  6769  enqbreq2  7441  ltanqg  7484  caucvgprprlemexb  7791  caucvgsrlemgt1  7879  caucvgsrlemoffres  7884  ltrennb  7938  apneg  8655  mulext1  8656  apdivmuld  8857  ltdiv23  8936  lediv23  8937  halfpos  9239  addltmul  9245  div4p1lem1div2  9262  ztri3or  9386  supminfex  9688  iccf1o  10096  fzshftral  10200  fzoshftral  10331  infssuzex  10340  2tnp1ge0ge0  10408  fihashen1  10908  seq3coll  10951  cjap  11088  negfi  11410  tanaddaplem  11920  dvdssub  12020  addmodlteqALT  12041  dvdsmod  12044  oddp1even  12058  nn0o1gt2  12087  nn0oddm1d2  12091  bitscmp  12140  cncongr1  12296  cncongr2  12297  4sqlem11  12595  4sqlem17  12601  intopsn  13069  sgrp1  13113  sgrppropd  13115  issubg  13379  nmzsubg  13416  conjnmzb  13486  srg1zr  13619  ring1  13691  issubrg  13853  znf1o  14283  znleval  14285  znunit  14291  elmopn  14766  metss  14814  comet  14819  xmetxp  14827  limcmpted  14983  cnlimc  14992  lgsneg  15349  lgsne0  15363  lgsprme0  15367  lgsquadlem1  15402  lgsquadlem2  15403  2lgs  15429  2lgsoddprm  15438