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  3087  sbcnel12g  3144  elxp4  5224  elxp5  5225  f1eq123d  5575  foeq123d  5576  f1oeq123d  5577  fnmptfvd  5751  ofrfval  6243  eloprabi  6360  fnmpoovd  6379  smoeq  6455  ecidg  6767  ixpsnval  6869  enqbreq2  7576  ltanqg  7619  caucvgprprlemexb  7926  caucvgsrlemgt1  8014  caucvgsrlemoffres  8019  ltrennb  8073  apneg  8790  mulext1  8791  apdivmuld  8992  ltdiv23  9071  lediv23  9072  halfpos  9374  addltmul  9380  div4p1lem1div2  9397  ztri3or  9521  supminfex  9830  iccf1o  10238  fzshftral  10342  fzoshftral  10483  infssuzex  10492  2tnp1ge0ge0  10560  fihashen1  11060  seq3coll  11105  s111  11207  swrdspsleq  11247  pfxeq  11276  wrd2ind  11303  cjap  11466  negfi  11788  tanaddaplem  12298  dvdssub  12398  addmodlteqALT  12419  dvdsmod  12422  oddp1even  12436  nn0o1gt2  12465  nn0oddm1d2  12469  bitscmp  12518  cncongr1  12674  cncongr2  12675  4sqlem11  12973  4sqlem17  12979  intopsn  13449  sgrp1  13493  sgrppropd  13495  issubg  13759  nmzsubg  13796  conjnmzb  13866  srg1zr  13999  ring1  14071  issubrg  14234  znf1o  14664  znleval  14666  znunit  14672  elmopn  15169  metss  15217  comet  15222  xmetxp  15230  limcmpted  15386  cnlimc  15395  lgsneg  15752  lgsne0  15766  lgsprme0  15770  lgsquadlem1  15805  lgsquadlem2  15806  2lgs  15832  2lgsoddprm  15841  edg0iedg0g  15916  wrdupgren  15946  wrdumgren  15956  vtxd0nedgbfi  16149  eupth2lem2dc  16309