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  3053  sbcnel12g  3109  elxp4  5169  elxp5  5170  f1eq123d  5513  foeq123d  5514  f1oeq123d  5515  fnmptfvd  5683  ofrfval  6166  eloprabi  6281  fnmpoovd  6300  smoeq  6375  ecidg  6685  ixpsnval  6787  enqbreq2  7469  ltanqg  7512  caucvgprprlemexb  7819  caucvgsrlemgt1  7907  caucvgsrlemoffres  7912  ltrennb  7966  apneg  8683  mulext1  8684  apdivmuld  8885  ltdiv23  8964  lediv23  8965  halfpos  9267  addltmul  9273  div4p1lem1div2  9290  ztri3or  9414  supminfex  9717  iccf1o  10125  fzshftral  10229  fzoshftral  10365  infssuzex  10374  2tnp1ge0ge0  10442  fihashen1  10942  seq3coll  10985  cjap  11159  negfi  11481  tanaddaplem  11991  dvdssub  12091  addmodlteqALT  12112  dvdsmod  12115  oddp1even  12129  nn0o1gt2  12158  nn0oddm1d2  12162  bitscmp  12211  cncongr1  12367  cncongr2  12368  4sqlem11  12666  4sqlem17  12672  intopsn  13141  sgrp1  13185  sgrppropd  13187  issubg  13451  nmzsubg  13488  conjnmzb  13558  srg1zr  13691  ring1  13763  issubrg  13925  znf1o  14355  znleval  14357  znunit  14363  elmopn  14860  metss  14908  comet  14913  xmetxp  14921  limcmpted  15077  cnlimc  15086  lgsneg  15443  lgsne0  15457  lgsprme0  15461  lgsquadlem1  15496  lgsquadlem2  15497  2lgs  15523  2lgsoddprm  15532