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  3058  sbcnel12g  3114  elxp4  5179  elxp5  5180  f1eq123d  5526  foeq123d  5527  f1oeq123d  5528  fnmptfvd  5697  ofrfval  6180  eloprabi  6295  fnmpoovd  6314  smoeq  6389  ecidg  6699  ixpsnval  6801  enqbreq2  7490  ltanqg  7533  caucvgprprlemexb  7840  caucvgsrlemgt1  7928  caucvgsrlemoffres  7933  ltrennb  7987  apneg  8704  mulext1  8705  apdivmuld  8906  ltdiv23  8985  lediv23  8986  halfpos  9288  addltmul  9294  div4p1lem1div2  9311  ztri3or  9435  supminfex  9738  iccf1o  10146  fzshftral  10250  fzoshftral  10389  infssuzex  10398  2tnp1ge0ge0  10466  fihashen1  10966  seq3coll  11009  s111  11108  swrdspsleq  11143  pfxeq  11172  wrd2ind  11199  cjap  11292  negfi  11614  tanaddaplem  12124  dvdssub  12224  addmodlteqALT  12245  dvdsmod  12248  oddp1even  12262  nn0o1gt2  12291  nn0oddm1d2  12295  bitscmp  12344  cncongr1  12500  cncongr2  12501  4sqlem11  12799  4sqlem17  12805  intopsn  13274  sgrp1  13318  sgrppropd  13320  issubg  13584  nmzsubg  13621  conjnmzb  13691  srg1zr  13824  ring1  13896  issubrg  14058  znf1o  14488  znleval  14490  znunit  14496  elmopn  14993  metss  15041  comet  15046  xmetxp  15054  limcmpted  15210  cnlimc  15219  lgsneg  15576  lgsne0  15590  lgsprme0  15594  lgsquadlem1  15629  lgsquadlem2  15630  2lgs  15656  2lgsoddprm  15665  edg0iedg0g  15737  wrdupgren  15767  wrdumgren  15777