Theorem 3bitr4rd 314

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 284	. 2 ⊢ (𝜑 → (𝜏 ↔ 𝜓))
4		3bitr4d.2	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜓))
5	3, 4	bitr4d 284	1 ⊢ (𝜑 → (𝜏 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  snssg  4710  inimasn  6007  isof1oidb  7071  oacan  8168  ecdmn0  8330  wemapwe  9154  r1pw  9268  adderpqlem  10370  mulerpqlem  10371  lterpq  10386  ltanq  10387  genpass  10425  readdcan  10808  lemuldiv  11514  msq11  11535  avglt2  11870  qbtwnre  12586  iooshf  12809  clim2c  14856  lo1o1  14883  climabs0  14936  reef11  15466  absefib  15545  efieq1re  15546  nndivides  15611  oddnn02np1  15691  oddge22np1  15692  evennn02n  15693  evennn2n  15694  halfleoddlt  15705  pc2dvds  16209  pcmpt  16222  subsubc  17117  odmulgid  18675  gexdvds  18703  submcmn2  18953  obslbs  20868  cnntr  21877  cndis  21893  cnindis  21894  cnpdis  21895  lmres  21902  cmpfi  22010  ist0-4  22331  txhmeo  22405  tsmssubm  22745  blin  23025  cncfmet  23510  icopnfcnv  23540  lmmbrf  23859  iscauf  23877  causs  23895  mbfposr  24247  itg2gt0  24355  limcflf  24473  limcres  24478  lhop1  24605  dvdsr1p  24749  fsumvma2  25784  vmasum  25786  chpchtsum  25789  bposlem1  25854  iscgrgd  26293  tgcgr4  26311  lnrot1  26403  eqeelen  26684  nbusgreledg  27129  nb3grprlem2  27157  wspthsnwspthsnon  27689  rusgrnumwwlks  27747  clwwlkwwlksb  27827  clwwlknwwlksnb  27828  dmdmd  30071  nfpconfp  30371  funcnvmpt  30406  1stpreimas  30435  xrdifh  30497  swrdrn3  30624  lsmsnorb  30940  ismntop  31262  eulerpartlemgh  31631  signslema  31827  fmlafvel  32627  topdifinfindis  34621  leceifl  34875  lindsadd  34879  lindsenlbs  34881  iblabsnclem  34949  ftc1anclem6  34966  areacirclem5  34980  areacirc  34981  brcoss3  35672  lsatfixedN  36139  cdlemg10c  37769  diaglbN  38185  dih1  38416  dihglbcpreN  38430  mapdcv  38790  ellz1  39357  islssfg  39663  proot1ex  39794  eliooshift  41775  clim2cf  41924  dfatdmfcoafv2  43447  sfprmdvdsmersenne  43762  odd2np1ALTV  43833  rrx2plordisom  44704