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  2959  sbcnel12g  3014  elxp4  5021  elxp5  5022  f1eq123d  5355  foeq123d  5356  f1oeq123d  5357  ofrfval  5983  eloprabi  6087  fnmpoovd  6105  smoeq  6180  ecidg  6486  ixpsnval  6588  enqbreq2  7158  ltanqg  7201  caucvgprprlemexb  7508  caucvgsrlemgt1  7596  caucvgsrlemoffres  7601  ltrennb  7655  apneg  8366  mulext1  8367  apdivmuld  8566  ltdiv23  8643  lediv23  8644  halfpos  8944  addltmul  8949  div4p1lem1div2  8966  ztri3or  9090  supminfex  9385  iccf1o  9780  fzshftral  9881  fzoshftral  10008  2tnp1ge0ge0  10067  fihashen1  10538  seq3coll  10578  cjap  10671  negfi  10992  tanaddaplem  11434  dvdssub  11527  addmodlteqALT  11546  dvdsmod  11549  oddp1even  11562  nn0o1gt2  11591  nn0oddm1d2  11595  infssuzex  11631  cncongr1  11773  cncongr2  11774  elmopn  12604  metss  12652  comet  12657  xmetxp  12665  limcmpted  12790  cnlimc  12799