Theorem 3bitr4rd 300

Description: Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)

Hypotheses

Ref	Expression
3bitr4d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
3bitr4d.2	⊢ (𝜑 → (𝜃 ↔ 𝜓))
3bitr4d.3	⊢ (𝜑 → (𝜏 ↔ 𝜒))

Assertion

Ref	Expression
3bitr4rd	⊢ (𝜑 → (𝜏 ↔ 𝜃))

Proof of Theorem 3bitr4rd

Step	Hyp	Ref	Expression
1		3bitr4d.3	. . 3 ⊢ (𝜑 → (𝜏 ↔ 𝜒))
2		3bitr4d.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	bitr4d 270	. 2 ⊢ (𝜑 → (𝜏 ↔ 𝜓))
4		3bitr4d.2	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜓))
5	3, 4	bitr4d 270	1 ⊢ (𝜑 → (𝜏 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 195

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 196

This theorem is referenced by:  inimasn  5469  isof1oidb  6474  oacan  7515  ecdmn0  7676  wemapwe  8477  r1pw  8591  adderpqlem  9655  mulerpqlem  9656  lterpq  9671  ltanq  9672  genpass  9710  readdcan  10089  lemuldiv  10782  msq11  10803  avglt2  11148  qbtwnre  11904  iooshf  12123  clim2c  14084  lo1o1  14111  climabs0  14164  reef11  14688  absefib  14767  efieq1re  14768  nndivides  14828  oddnn02np1  14910  oddge22np1  14911  evennn02n  14912  evennn2n  14913  halfleoddlt  14924  pc2dvds  15421  pcmpt  15434  subsubc  16336  odmulgid  17794  gexdvds  17822  submcmn2  18067  obslbs  19893  cnntr  20889  cndis  20905  cnindis  20906  cnpdis  20907  lmres  20914  cmpfi  21021  ist0-4  21342  txhmeo  21416  tsmssubm  21756  blin  22036  cncfmet  22519  icopnfcnv  22549  lmmbrf  22868  iscauf  22886  causs  22904  mbfposr  23225  itg2gt0  23333  limcflf  23451  limcres  23456  lhop1  23581  dvdsr1p  23725  fsumvma2  24739  vmasum  24741  chpchtsum  24744  bposlem1  24809  iscgrgd  25208  tgcgr4  25226  lnrot1  25318  eqeelen  25584  nbgraeledg  25959  nb3graprlem2  25981  cusgra3v  25993  cusgrauvtxb  26024  clwlkisclwwlk2  26318  el2spthonot0  26398  rusgranumwlks  26483  dmdmd  28543  funcnvmptOLD  28850  funcnvmpt  28851  1stpreimas  28866  xrdifh  28932  ismntop  29398  eulerpartlemgh  29767  signslema  29965  topdifinfindis  32370  leceifl  32568  lindsenlbs  32574  iblabsnclem  32643  ftc1anclem6  32660  areacirclem5  32674  areacirc  32675  lsatfixedN  33314  cdlemg10c  34945  diaglbN  35362  dih1  35593  dihglbcpreN  35607  mapdcv  35967  ellz1  36348  islssfg  36658  proot1ex  36798  eliooshift  38576  clim2cf  38717  sfprmdvdsmersenne  40058  odd2np1ALTV  40123  nbusgreledg  40575  nb3grprlem2  40609  wspthsnwspthsnon  41122  rusgrnumwwlks  41177  clwlkclwwlk2  41212