Theorem 3bitr4rd 312

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  snssgOLD  4748  inimasn  6129  isof1oidb  7299  oacan  8512  ecdmn0  8723  wemapwe  9650  ttrclselem2  9679  r1pw  9798  adderpqlem  10907  mulerpqlem  10908  lterpq  10923  ltanq  10924  genpass  10962  readdcan  11348  lemuldiv  12063  msq11  12084  avglt2  12421  qbtwnre  13159  iooshf  13387  clim2c  15471  lo1o1  15498  climabs0  15551  reef11  16087  absefib  16166  efieq1re  16167  nndivides  16232  oddnn02np1  16318  oddge22np1  16319  evennn02n  16320  evennn2n  16321  halfleoddlt  16332  pc2dvds  16850  pcmpt  16863  subsubc  17815  ghmqusker  19219  odmulgid  19484  gexdvds  19514  submcmn2  19769  obslbs  21639  cnntr  23162  cndis  23178  cnindis  23179  cnpdis  23180  lmres  23187  cmpfi  23295  ist0-4  23616  txhmeo  23690  tsmssubm  24030  blin  24309  cncfmet  24802  icopnfcnv  24840  lmmbrf  25162  iscauf  25180  causs  25198  mbfposr  25553  itg2gt0  25661  limcflf  25782  limcres  25787  lhop1  25919  dvdsr1p  26069  fsumvma2  27125  vmasum  27127  chpchtsum  27130  bposlem1  27195  addscan2  27900  slesubaddd  27997  mulscan2dlem  28081  iscgrgd  28440  tgcgr4  28458  lnrot1  28550  eqeelen  28831  nbusgreledg  29280  nb3grprlem2  29308  wspthsnwspthsnon  29846  rusgrnumwwlks  29904  clwwlkwwlksb  29983  clwwlknwwlksnb  29984  dmdmd  32229  nfpconfp  32556  funcnvmpt  32591  1stpreimas  32629  xrdifh  32703  swrdrn3  32877  lsmsnorb  33362  fldextrspunlsp  33669  rhmpreimacnlem  33874  ismntop  34016  eulerpartlemgh  34369  signslema  34553  fmlafvel  35372  topdifinfindis  37334  leceifl  37603  lindsadd  37607  lindsenlbs  37609  iblabsnclem  37677  ftc1anclem6  37692  areacirclem5  37706  areacirc  37707  brcoss3  38424  lsatfixedN  39002  cdlemg10c  40633  diaglbN  41049  dih1  41280  dihglbcpreN  41294  mapdcv  41654  dvdsexpnn0  42322  ef11d  42327  ellz1  42755  islssfg  43059  proot1ex  43185  tfsconcat00  43336  eliooshift  45504  clim2cf  45648  dfatdmfcoafv2  47255  sfprmdvdsmersenne  47604  odd2np1ALTV  47675  vopnbgrelself  47855  rrx2plordisom  48712  i0oii  48908  io1ii  48909  oppccic  49033  uptrlem3  49201  uptr2  49210