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  3088  sbcnel12g  3145  elxp4  5231  elxp5  5232  f1eq123d  5584  foeq123d  5585  f1oeq123d  5586  fnmptfvd  5760  ofrfval  6253  eloprabi  6370  fnmpoovd  6389  suppsnopdc  6428  smoeq  6499  ecidg  6811  ixpsnval  6913  enqbreq2  7620  ltanqg  7663  caucvgprprlemexb  7970  caucvgsrlemgt1  8058  caucvgsrlemoffres  8063  ltrennb  8117  apneg  8833  mulext1  8834  apdivmuld  9035  ltdiv23  9114  lediv23  9115  halfpos  9417  addltmul  9423  div4p1lem1div2  9440  ztri3or  9566  supminfex  9875  iccf1o  10284  fzshftral  10388  fzoshftral  10530  infssuzex  10539  2tnp1ge0ge0  10607  fihashen1  11107  seq3coll  11152  s111  11257  swrdspsleq  11297  pfxeq  11326  wrd2ind  11353  cjap  11529  negfi  11851  tanaddaplem  12362  dvdssub  12462  addmodlteqALT  12483  dvdsmod  12486  oddp1even  12500  nn0o1gt2  12529  nn0oddm1d2  12533  bitscmp  12582  cncongr1  12738  cncongr2  12739  4sqlem11  13037  4sqlem17  13043  intopsn  13513  sgrp1  13557  sgrppropd  13559  issubg  13823  nmzsubg  13860  conjnmzb  13930  srg1zr  14064  ring1  14136  issubrg  14299  znf1o  14730  znleval  14732  znunit  14738  elmopn  15240  metss  15288  comet  15293  xmetxp  15301  limcmpted  15457  cnlimc  15466  lgsneg  15826  lgsne0  15840  lgsprme0  15844  lgsquadlem1  15879  lgsquadlem2  15880  2lgs  15906  2lgsoddprm  15915  edg0iedg0g  15990  wrdupgren  16020  wrdumgren  16030  vtxd0nedgbfi  16223  eupth2lem2dc  16383  eupth2lem3lem6fi  16395  eupth2lem3lem4fi  16397