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  3045  sbcnel12g  3101  elxp4  5158  elxp5  5159  f1eq123d  5499  foeq123d  5500  f1oeq123d  5501  fnmptfvd  5669  ofrfval  6148  eloprabi  6263  fnmpoovd  6282  smoeq  6357  ecidg  6667  ixpsnval  6769  enqbreq2  7443  ltanqg  7486  caucvgprprlemexb  7793  caucvgsrlemgt1  7881  caucvgsrlemoffres  7886  ltrennb  7940  apneg  8657  mulext1  8658  apdivmuld  8859  ltdiv23  8938  lediv23  8939  halfpos  9241  addltmul  9247  div4p1lem1div2  9264  ztri3or  9388  supminfex  9690  iccf1o  10098  fzshftral  10202  fzoshftral  10333  infssuzex  10342  2tnp1ge0ge0  10410  fihashen1  10910  seq3coll  10953  cjap  11090  negfi  11412  tanaddaplem  11922  dvdssub  12022  addmodlteqALT  12043  dvdsmod  12046  oddp1even  12060  nn0o1gt2  12089  nn0oddm1d2  12093  bitscmp  12142  cncongr1  12298  cncongr2  12299  4sqlem11  12597  4sqlem17  12603  intopsn  13071  sgrp1  13115  sgrppropd  13117  issubg  13381  nmzsubg  13418  conjnmzb  13488  srg1zr  13621  ring1  13693  issubrg  13855  znf1o  14285  znleval  14287  znunit  14293  elmopn  14790  metss  14838  comet  14843  xmetxp  14851  limcmpted  15007  cnlimc  15016  lgsneg  15373  lgsne0  15387  lgsprme0  15391  lgsquadlem1  15426  lgsquadlem2  15427  2lgs  15453  2lgsoddprm  15462