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  6244  eloprabi  6361  fnmpoovd  6380  smoeq  6456  ecidg  6768  ixpsnval  6870  enqbreq2  7577  ltanqg  7620  caucvgprprlemexb  7927  caucvgsrlemgt1  8015  caucvgsrlemoffres  8020  ltrennb  8074  apneg  8791  mulext1  8792  apdivmuld  8993  ltdiv23  9072  lediv23  9073  halfpos  9375  addltmul  9381  div4p1lem1div2  9398  ztri3or  9522  supminfex  9831  iccf1o  10239  fzshftral  10343  fzoshftral  10485  infssuzex  10494  2tnp1ge0ge0  10562  fihashen1  11062  seq3coll  11107  s111  11212  swrdspsleq  11252  pfxeq  11281  wrd2ind  11308  cjap  11484  negfi  11806  tanaddaplem  12317  dvdssub  12417  addmodlteqALT  12438  dvdsmod  12441  oddp1even  12455  nn0o1gt2  12484  nn0oddm1d2  12488  bitscmp  12537  cncongr1  12693  cncongr2  12694  4sqlem11  12992  4sqlem17  12998  intopsn  13468  sgrp1  13512  sgrppropd  13514  issubg  13778  nmzsubg  13815  conjnmzb  13885  srg1zr  14019  ring1  14091  issubrg  14254  znf1o  14684  znleval  14686  znunit  14692  elmopn  15189  metss  15237  comet  15242  xmetxp  15250  limcmpted  15406  cnlimc  15415  lgsneg  15772  lgsne0  15786  lgsprme0  15790  lgsquadlem1  15825  lgsquadlem2  15826  2lgs  15852  2lgsoddprm  15861  edg0iedg0g  15936  wrdupgren  15966  wrdumgren  15976  vtxd0nedgbfi  16169  eupth2lem2dc  16329  eupth2lem3lem6fi  16341  eupth2lem3lem4fi  16343