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  6111  isof1oidb  7267  oacan  8472  ecdmn0  8683  wemapwe  9598  ttrclselem2  9627  r1pw  9749  adderpqlem  10856  mulerpqlem  10857  lterpq  10872  ltanq  10873  genpass  10911  readdcan  11298  lemuldiv  12013  msq11  12034  avglt2  12371  qbtwnre  13105  iooshf  13333  clim2c  15419  lo1o1  15446  climabs0  15499  reef11  16035  absefib  16114  efieq1re  16115  nndivides  16180  oddnn02np1  16266  oddge22np1  16267  evennn02n  16268  evennn2n  16269  halfleoddlt  16280  pc2dvds  16798  pcmpt  16811  subsubc  17768  ghmqusker  19207  odmulgid  19474  gexdvds  19504  submcmn2  19759  obslbs  21676  cnntr  23210  cndis  23226  cnindis  23227  cnpdis  23228  lmres  23235  cmpfi  23343  ist0-4  23664  txhmeo  23738  tsmssubm  24078  blin  24356  cncfmet  24849  icopnfcnv  24887  lmmbrf  25209  iscauf  25227  causs  25245  mbfposr  25600  itg2gt0  25708  limcflf  25829  limcres  25834  lhop1  25966  dvdsr1p  26116  fsumvma2  27172  vmasum  27174  chpchtsum  27177  bposlem1  27242  addscan2  27956  slesubaddd  28053  mulscan2dlem  28137  iscgrgd  28511  tgcgr4  28529  lnrot1  28621  eqeelen  28903  nbusgreledg  29352  nb3grprlem2  29380  wspthsnwspthsnon  29915  rusgrnumwwlks  29976  clwwlkwwlksb  30055  clwwlknwwlksnb  30056  dmdmd  32301  nfpconfp  32636  funcnvmpt  32671  1stpreimas  32711  xrdifh  32788  swrdrn3  32965  lsmsnorb  33400  fldextrspunlsp  33759  rhmpreimacnlem  33969  ismntop  34111  eulerpartlemgh  34463  signslema  34647  fmlafvel  35501  topdifinfindis  37463  leceifl  37722  lindsadd  37726  lindsenlbs  37728  iblabsnclem  37796  ftc1anclem6  37811  areacirclem5  37825  areacirc  37826  brcoss3  38608  lsatfixedN  39181  cdlemg10c  40811  diaglbN  41227  dih1  41458  dihglbcpreN  41472  mapdcv  41832  dvdsexpnn0  42504  ef11d  42509  ellz1  42924  islssfg  43227  proot1ex  43353  tfsconcat00  43504  eliooshift  45668  clim2cf  45810  dfatdmfcoafv2  47416  sfprmdvdsmersenne  47765  odd2np1ALTV  47836  vopnbgrelself  48017  rrx2plordisom  48885  i0oii  49081  io1ii  49082  oppccic  49205  uptrlem3  49373  uptr2  49382