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  3085  sbcnel12g  3142  elxp4  5222  elxp5  5223  f1eq123d  5572  foeq123d  5573  f1oeq123d  5574  fnmptfvd  5747  ofrfval  6239  eloprabi  6356  fnmpoovd  6375  smoeq  6451  ecidg  6763  ixpsnval  6865  enqbreq2  7567  ltanqg  7610  caucvgprprlemexb  7917  caucvgsrlemgt1  8005  caucvgsrlemoffres  8010  ltrennb  8064  apneg  8781  mulext1  8782  apdivmuld  8983  ltdiv23  9062  lediv23  9063  halfpos  9365  addltmul  9371  div4p1lem1div2  9388  ztri3or  9512  supminfex  9821  iccf1o  10229  fzshftral  10333  fzoshftral  10474  infssuzex  10483  2tnp1ge0ge0  10551  fihashen1  11051  seq3coll  11096  s111  11198  swrdspsleq  11238  pfxeq  11267  wrd2ind  11294  cjap  11457  negfi  11779  tanaddaplem  12289  dvdssub  12389  addmodlteqALT  12410  dvdsmod  12413  oddp1even  12427  nn0o1gt2  12456  nn0oddm1d2  12460  bitscmp  12509  cncongr1  12665  cncongr2  12666  4sqlem11  12964  4sqlem17  12970  intopsn  13440  sgrp1  13484  sgrppropd  13486  issubg  13750  nmzsubg  13787  conjnmzb  13857  srg1zr  13990  ring1  14062  issubrg  14225  znf1o  14655  znleval  14657  znunit  14663  elmopn  15160  metss  15208  comet  15213  xmetxp  15221  limcmpted  15377  cnlimc  15386  lgsneg  15743  lgsne0  15757  lgsprme0  15761  lgsquadlem1  15796  lgsquadlem2  15797  2lgs  15823  2lgsoddprm  15832  edg0iedg0g  15907  wrdupgren  15937  wrdumgren  15947  vtxd0nedgbfi  16105