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  4751  inimasn  6132  isof1oidb  7302  oacan  8515  ecdmn0  8726  wemapwe  9657  ttrclselem2  9686  r1pw  9805  adderpqlem  10914  mulerpqlem  10915  lterpq  10930  ltanq  10931  genpass  10969  readdcan  11355  lemuldiv  12070  msq11  12091  avglt2  12428  qbtwnre  13166  iooshf  13394  clim2c  15478  lo1o1  15505  climabs0  15558  reef11  16094  absefib  16173  efieq1re  16174  nndivides  16239  oddnn02np1  16325  oddge22np1  16326  evennn02n  16327  evennn2n  16328  halfleoddlt  16339  pc2dvds  16857  pcmpt  16870  subsubc  17822  ghmqusker  19226  odmulgid  19491  gexdvds  19521  submcmn2  19776  obslbs  21646  cnntr  23169  cndis  23185  cnindis  23186  cnpdis  23187  lmres  23194  cmpfi  23302  ist0-4  23623  txhmeo  23697  tsmssubm  24037  blin  24316  cncfmet  24809  icopnfcnv  24847  lmmbrf  25169  iscauf  25187  causs  25205  mbfposr  25560  itg2gt0  25668  limcflf  25789  limcres  25794  lhop1  25926  dvdsr1p  26076  fsumvma2  27132  vmasum  27134  chpchtsum  27137  bposlem1  27202  addscan2  27907  slesubaddd  28004  mulscan2dlem  28088  iscgrgd  28447  tgcgr4  28465  lnrot1  28557  eqeelen  28838  nbusgreledg  29287  nb3grprlem2  29315  wspthsnwspthsnon  29853  rusgrnumwwlks  29911  clwwlkwwlksb  29990  clwwlknwwlksnb  29991  dmdmd  32236  nfpconfp  32563  funcnvmpt  32598  1stpreimas  32636  xrdifh  32710  swrdrn3  32884  lsmsnorb  33369  fldextrspunlsp  33676  rhmpreimacnlem  33881  ismntop  34023  eulerpartlemgh  34376  signslema  34560  fmlafvel  35379  topdifinfindis  37341  leceifl  37610  lindsadd  37614  lindsenlbs  37616  iblabsnclem  37684  ftc1anclem6  37699  areacirclem5  37713  areacirc  37714  brcoss3  38431  lsatfixedN  39009  cdlemg10c  40640  diaglbN  41056  dih1  41287  dihglbcpreN  41301  mapdcv  41661  dvdsexpnn0  42329  ef11d  42334  ellz1  42762  islssfg  43066  proot1ex  43192  tfsconcat00  43343  eliooshift  45511  clim2cf  45655  dfatdmfcoafv2  47259  sfprmdvdsmersenne  47608  odd2np1ALTV  47679  vopnbgrelself  47859  rrx2plordisom  48716  i0oii  48912  io1ii  48913  oppccic  49037  uptrlem3  49205  uptr2  49214