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  3011  sbcnel12g  3067  elxp4  5100  elxp5  5101  f1eq123d  5437  foeq123d  5438  f1oeq123d  5439  fnmptfvd  5604  ofrfval  6073  eloprabi  6179  fnmpoovd  6198  smoeq  6273  ecidg  6581  ixpsnval  6683  enqbreq2  7323  ltanqg  7366  caucvgprprlemexb  7673  caucvgsrlemgt1  7761  caucvgsrlemoffres  7766  ltrennb  7820  apneg  8534  mulext1  8535  apdivmuld  8734  ltdiv23  8812  lediv23  8813  halfpos  9113  addltmul  9118  div4p1lem1div2  9135  ztri3or  9259  supminfex  9560  iccf1o  9965  fzshftral  10068  fzoshftral  10198  2tnp1ge0ge0  10261  fihashen1  10738  seq3coll  10781  cjap  10874  negfi  11195  tanaddaplem  11705  dvdssub  11804  addmodlteqALT  11823  dvdsmod  11826  oddp1even  11839  nn0o1gt2  11868  nn0oddm1d2  11872  infssuzex  11908  cncongr1  12061  cncongr2  12062  intopsn  12625  sgrp1  12655  elmopn  13325  metss  13373  comet  13378  xmetxp  13386  limcmpted  13511  cnlimc  13520  lgsneg  13804  lgsne0  13818  lgsprme0  13822