Theorem 3bitr4rd 311

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  snssgOLD  4793  inimasn  6167  isof1oidb  7336  oacan  8578  ecdmn0  8783  wemapwe  9740  ttrclselem2  9769  r1pw  9888  adderpqlem  10997  mulerpqlem  10998  lterpq  11013  ltanq  11014  genpass  11052  readdcan  11438  lemuldiv  12146  msq11  12167  avglt2  12503  qbtwnre  13232  iooshf  13457  clim2c  15507  lo1o1  15534  climabs0  15587  reef11  16121  absefib  16200  efieq1re  16201  nndivides  16266  oddnn02np1  16350  oddge22np1  16351  evennn02n  16352  evennn2n  16353  halfleoddlt  16364  pc2dvds  16881  pcmpt  16894  subsubc  17872  ghmqusker  19281  odmulgid  19552  gexdvds  19582  submcmn2  19837  obslbs  21728  cnntr  23270  cndis  23286  cnindis  23287  cnpdis  23288  lmres  23295  cmpfi  23403  ist0-4  23724  txhmeo  23798  tsmssubm  24138  blin  24418  cncfmet  24920  icopnfcnv  24958  lmmbrf  25281  iscauf  25299  causs  25317  mbfposr  25672  itg2gt0  25781  limcflf  25901  limcres  25906  lhop1  26038  dvdsr1p  26191  fsumvma2  27243  vmasum  27245  chpchtsum  27248  bposlem1  27313  addscan2  28007  slesubaddd  28100  mulscan2dlem  28179  iscgrgd  28440  tgcgr4  28458  lnrot1  28550  eqeelen  28838  nbusgreledg  29289  nb3grprlem2  29317  wspthsnwspthsnon  29850  rusgrnumwwlks  29908  clwwlkwwlksb  29987  clwwlknwwlksnb  29988  dmdmd  32233  nfpconfp  32549  funcnvmpt  32584  1stpreimas  32617  xrdifh  32682  swrdrn3  32819  lsmsnorb  33266  rhmpreimacnlem  33699  ismntop  33841  eulerpartlemgh  34212  signslema  34408  fmlafvel  35213  topdifinfindis  37053  leceifl  37310  lindsadd  37314  lindsenlbs  37316  iblabsnclem  37384  ftc1anclem6  37399  areacirclem5  37413  areacirc  37414  brcoss3  38131  lsatfixedN  38707  cdlemg10c  40338  diaglbN  40754  dih1  40985  dihglbcpreN  40999  mapdcv  41359  dvdsexpnn0  42129  ef11d  42135  ellz1  42424  islssfg  42731  proot1ex  42861  tfsconcat00  43013  eliooshift  45124  clim2cf  45271  dfatdmfcoafv2  46867  sfprmdvdsmersenne  47175  odd2np1ALTV  47246  vopnbgrelself  47422  rrx2plordisom  48111  i0oii  48253  io1ii  48254