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  3018  sbcnel12g  3074  elxp4  5115  elxp5  5116  f1eq123d  5452  foeq123d  5453  f1oeq123d  5454  fnmptfvd  5619  ofrfval  6088  eloprabi  6194  fnmpoovd  6213  smoeq  6288  ecidg  6596  ixpsnval  6698  enqbreq2  7353  ltanqg  7396  caucvgprprlemexb  7703  caucvgsrlemgt1  7791  caucvgsrlemoffres  7796  ltrennb  7850  apneg  8564  mulext1  8565  apdivmuld  8766  ltdiv23  8845  lediv23  8846  halfpos  9146  addltmul  9151  div4p1lem1div2  9168  ztri3or  9292  supminfex  9593  iccf1o  10000  fzshftral  10103  fzoshftral  10233  2tnp1ge0ge0  10296  fihashen1  10772  seq3coll  10815  cjap  10908  negfi  11229  tanaddaplem  11739  dvdssub  11838  addmodlteqALT  11857  dvdsmod  11860  oddp1even  11873  nn0o1gt2  11902  nn0oddm1d2  11906  infssuzex  11942  cncongr1  12095  cncongr2  12096  intopsn  12718  sgrp1  12748  issubg  12964  nmzsubg  13001  srg1zr  13101  ring1  13167  issubrg  13280  elmopn  13817  metss  13865  comet  13870  xmetxp  13878  limcmpted  14003  cnlimc  14012  lgsneg  14296  lgsne0  14310  lgsprme0  14314