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-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sbceqal  2932  sbcnel12g  2986  elxp4  4984  elxp5  4985  f1eq123d  5318  foeq123d  5319  f1oeq123d  5320  ofrfval  5944  eloprabi  6048  fnmpoovd  6066  smoeq  6141  ecidg  6447  ixpsnval  6549  enqbreq2  7110  ltanqg  7153  caucvgprprlemexb  7460  caucvgsrlemgt1  7534  caucvgsrlemoffres  7539  ltrennb  7586  apneg  8288  mulext1  8289  apdivmuld  8483  ltdiv23  8557  lediv23  8558  halfpos  8852  addltmul  8857  div4p1lem1div2  8874  ztri3or  8998  supminfex  9291  iccf1o  9677  fzshftral  9778  fzoshftral  9905  2tnp1ge0ge0  9964  fihashen1  10435  seq3coll  10475  cjap  10568  negfi  10888  tanaddaplem  11293  dvdssub  11383  addmodlteqALT  11402  dvdsmod  11405  oddp1even  11418  nn0o1gt2  11447  nn0oddm1d2  11451  infssuzex  11487  cncongr1  11627  cncongr2  11628  elmopn  12432  metss  12480  comet  12485  xmetxp  12493  limcmpted  12585  cnlimc  12594