Theorem 3bitrd 213

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 187	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4		3bitrd.3	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
5	3, 4	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:  sbceqal  2992  sbcnel12g  3048  elxp4  5070  elxp5  5071  f1eq123d  5404  foeq123d  5405  f1oeq123d  5406  ofrfval  6034  eloprabi  6138  fnmpoovd  6156  smoeq  6231  ecidg  6537  ixpsnval  6639  enqbreq2  7260  ltanqg  7303  caucvgprprlemexb  7610  caucvgsrlemgt1  7698  caucvgsrlemoffres  7703  ltrennb  7757  apneg  8469  mulext1  8470  apdivmuld  8669  ltdiv23  8746  lediv23  8747  halfpos  9047  addltmul  9052  div4p1lem1div2  9069  ztri3or  9193  supminfex  9491  iccf1o  9890  fzshftral  9992  fzoshftral  10119  2tnp1ge0ge0  10182  fihashen1  10655  seq3coll  10695  cjap  10788  negfi  11109  tanaddaplem  11617  dvdssub  11713  addmodlteqALT  11732  dvdsmod  11735  oddp1even  11748  nn0o1gt2  11777  nn0oddm1d2  11781  infssuzex  11817  cncongr1  11960  cncongr2  11961  elmopn  12806  metss  12854  comet  12859  xmetxp  12867  limcmpted  12992  cnlimc  13001