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:  inimasn  6122  funcnvmpt  6951  isof1oidb  7280  oacan  8485  ecdmn0  8698  wemapwe  9618  ttrclselem2  9647  r1pw  9769  adderpqlem  10877  mulerpqlem  10878  lterpq  10893  ltanq  10894  genpass  10932  readdcan  11319  lemuldiv  12034  msq11  12055  avglt2  12392  qbtwnre  13126  iooshf  13354  clim2c  15440  lo1o1  15467  climabs0  15520  reef11  16056  absefib  16135  efieq1re  16136  nndivides  16201  oddnn02np1  16287  oddge22np1  16288  evennn02n  16289  evennn2n  16290  halfleoddlt  16301  pc2dvds  16819  pcmpt  16832  subsubc  17789  ghmqusker  19228  odmulgid  19495  gexdvds  19525  submcmn2  19780  obslbs  21697  cnntr  23231  cndis  23247  cnindis  23248  cnpdis  23249  lmres  23256  cmpfi  23364  ist0-4  23685  txhmeo  23759  tsmssubm  24099  blin  24377  cncfmet  24870  icopnfcnv  24908  lmmbrf  25230  iscauf  25248  causs  25266  mbfposr  25621  itg2gt0  25729  limcflf  25850  limcres  25855  lhop1  25987  dvdsr1p  26137  fsumvma2  27193  vmasum  27195  chpchtsum  27198  bposlem1  27263  addscan2  28001  lesubaddsd  28101  mulscan2dlem  28186  bdayfinbndlem1  28475  iscgrgd  28597  tgcgr4  28615  lnrot1  28707  eqeelen  28989  nbusgreledg  29438  nb3grprlem2  29466  wspthsnwspthsnon  30001  rusgrnumwwlks  30062  clwwlkwwlksb  30141  clwwlknwwlksnb  30142  dmdmd  32387  nfpconfp  32721  1stpreimas  32795  xrdifh  32870  swrdrn3  33047  lsmsnorb  33483  esplyfval1  33749  fldextrspunlsp  33851  rhmpreimacnlem  34061  ismntop  34203  eulerpartlemgh  34555  signslema  34739  fmlafvel  35598  topdifinfindis  37598  leceifl  37857  lindsadd  37861  lindsenlbs  37863  iblabsnclem  37931  ftc1anclem6  37946  areacirclem5  37960  areacirc  37961  brcoss3  38771  lsatfixedN  39382  cdlemg10c  41012  diaglbN  41428  dih1  41659  dihglbcpreN  41673  mapdcv  42033  dvdsexpnn0  42701  ef11d  42706  ellz1  43121  islssfg  43424  proot1ex  43550  tfsconcat00  43701  eliooshift  45863  clim2cf  46005  dfatdmfcoafv2  47611  sfprmdvdsmersenne  47960  odd2np1ALTV  48031  vopnbgrelself  48212  rrx2plordisom  49080  i0oii  49276  io1ii  49277  oppccic  49400  uptrlem3  49568  uptr2  49577