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  3084  sbcnel12g  3141  elxp4  5216  elxp5  5217  f1eq123d  5566  foeq123d  5567  f1oeq123d  5568  fnmptfvd  5741  ofrfval  6233  eloprabi  6348  fnmpoovd  6367  smoeq  6442  ecidg  6754  ixpsnval  6856  enqbreq2  7555  ltanqg  7598  caucvgprprlemexb  7905  caucvgsrlemgt1  7993  caucvgsrlemoffres  7998  ltrennb  8052  apneg  8769  mulext1  8770  apdivmuld  8971  ltdiv23  9050  lediv23  9051  halfpos  9353  addltmul  9359  div4p1lem1div2  9376  ztri3or  9500  supminfex  9804  iccf1o  10212  fzshftral  10316  fzoshftral  10456  infssuzex  10465  2tnp1ge0ge0  10533  fihashen1  11033  seq3coll  11077  s111  11179  swrdspsleq  11214  pfxeq  11243  wrd2ind  11270  cjap  11432  negfi  11754  tanaddaplem  12264  dvdssub  12364  addmodlteqALT  12385  dvdsmod  12388  oddp1even  12402  nn0o1gt2  12431  nn0oddm1d2  12435  bitscmp  12484  cncongr1  12640  cncongr2  12641  4sqlem11  12939  4sqlem17  12945  intopsn  13415  sgrp1  13459  sgrppropd  13461  issubg  13725  nmzsubg  13762  conjnmzb  13832  srg1zr  13965  ring1  14037  issubrg  14200  znf1o  14630  znleval  14632  znunit  14638  elmopn  15135  metss  15183  comet  15188  xmetxp  15196  limcmpted  15352  cnlimc  15361  lgsneg  15718  lgsne0  15732  lgsprme0  15736  lgsquadlem1  15771  lgsquadlem2  15772  2lgs  15798  2lgsoddprm  15807  edg0iedg0g  15881  wrdupgren  15911  wrdumgren  15921