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  3101  sbcnel12g  3158  elxp4  5255  elxp5  5256  f1eq123d  5611  foeq123d  5612  f1oeq123d  5613  fnmptfvd  5787  ofrfval  6284  eloprabi  6405  fnmpoovd  6424  suppsnopdc  6463  smoeq  6534  ecidg  6846  ixpsnval  6949  mapsnend  7065  enqbreq2  7688  ltanqg  7731  caucvgprprlemexb  8038  caucvgsrlemgt1  8126  caucvgsrlemoffres  8131  ltrennb  8185  apneg  8902  mulext1  8903  apdivmuld  9104  ltdiv23  9183  lediv23  9184  halfpos  9486  addltmul  9492  div4p1lem1div2  9509  ztri3or  9637  supminfex  9947  iccf1o  10357  fzsplit3  10407  fzshftral  10464  fzoshftral  10606  infssuzex  10615  2tnp1ge0ge0  10685  fihashen1  11187  seq3coll  11239  s111  11344  swrdspsleq  11384  pfxeq  11413  wrd2ind  11440  cjap  11616  negfi  11938  tanaddaplem  12449  dvdssub  12549  addmodlteqALT  12570  dvdsmod  12573  oddp1even  12587  nn0o1gt2  12616  nn0oddm1d2  12620  bitscmp  12669  cncongr1  12825  cncongr2  12826  4sqlem11  13124  4sqlem17  13130  ballotfilemsima  13203  intopsn  13630  sgrp1  13674  sgrppropd  13676  issubg  13926  nmzsubg  13963  conjnmzb  14033  rng1zrlem  14198  ring1  14302  issubrg  14467  znf1o  14925  znleval  14927  znunit  14933  elmopn  15437  metss  15485  comet  15490  xmetxp  15498  limcmpted  15654  cnlimc  15663  lgsneg  16023  lgsne0  16037  lgsprme0  16041  lgsquadlem1  16076  lgsquadlem2  16077  2lgs  16103  2lgsoddprm  16112  edg0iedg0g  16187  wrdupgren  16217  wrdumgren  16227  vtxd0nedgbfi  16420  eupth2lem2dc  16580  eupth2lem3lem6fi  16592  eupth2lem3lem4fi  16594