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  5215  elxp5  5216  f1eq123d  5563  foeq123d  5564  f1oeq123d  5565  fnmptfvd  5738  ofrfval  6225  eloprabi  6340  fnmpoovd  6359  smoeq  6434  ecidg  6744  ixpsnval  6846  enqbreq2  7540  ltanqg  7583  caucvgprprlemexb  7890  caucvgsrlemgt1  7978  caucvgsrlemoffres  7983  ltrennb  8037  apneg  8754  mulext1  8755  apdivmuld  8956  ltdiv23  9035  lediv23  9036  halfpos  9338  addltmul  9344  div4p1lem1div2  9361  ztri3or  9485  supminfex  9788  iccf1o  10196  fzshftral  10300  fzoshftral  10439  infssuzex  10448  2tnp1ge0ge0  10516  fihashen1  11016  seq3coll  11059  s111  11159  swrdspsleq  11194  pfxeq  11223  wrd2ind  11250  cjap  11412  negfi  11734  tanaddaplem  12244  dvdssub  12344  addmodlteqALT  12365  dvdsmod  12368  oddp1even  12382  nn0o1gt2  12411  nn0oddm1d2  12415  bitscmp  12464  cncongr1  12620  cncongr2  12621  4sqlem11  12919  4sqlem17  12925  intopsn  13395  sgrp1  13439  sgrppropd  13441  issubg  13705  nmzsubg  13742  conjnmzb  13812  srg1zr  13945  ring1  14017  issubrg  14179  znf1o  14609  znleval  14611  znunit  14617  elmopn  15114  metss  15162  comet  15167  xmetxp  15175  limcmpted  15331  cnlimc  15340  lgsneg  15697  lgsne0  15711  lgsprme0  15715  lgsquadlem1  15750  lgsquadlem2  15751  2lgs  15777  2lgsoddprm  15786  edg0iedg0g  15860  wrdupgren  15890  wrdumgren  15900