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  4787  inimasn  6154  isof1oidb  7323  oacan  8550  ecdmn0  8752  wemapwe  9694  ttrclselem2  9723  r1pw  9842  adderpqlem  10951  mulerpqlem  10952  lterpq  10967  ltanq  10968  genpass  11006  readdcan  11392  lemuldiv  12098  msq11  12119  avglt2  12455  qbtwnre  13182  iooshf  13407  clim2c  15453  lo1o1  15480  climabs0  15533  reef11  16066  absefib  16145  efieq1re  16146  nndivides  16211  oddnn02np1  16295  oddge22np1  16296  evennn02n  16297  evennn2n  16298  halfleoddlt  16309  pc2dvds  16816  pcmpt  16829  subsubc  17807  odmulgid  19463  gexdvds  19493  submcmn2  19748  obslbs  21504  cnntr  22999  cndis  23015  cnindis  23016  cnpdis  23017  lmres  23024  cmpfi  23132  ist0-4  23453  txhmeo  23527  tsmssubm  23867  blin  24147  cncfmet  24649  icopnfcnv  24687  lmmbrf  25010  iscauf  25028  causs  25046  mbfposr  25401  itg2gt0  25510  limcflf  25630  limcres  25635  lhop1  25766  dvdsr1p  25914  fsumvma2  26953  vmasum  26955  chpchtsum  26958  bposlem1  27023  addscan2  27715  mulscan2dlem  27869  iscgrgd  28031  tgcgr4  28049  lnrot1  28141  eqeelen  28429  nbusgreledg  28877  nb3grprlem2  28905  wspthsnwspthsnon  29437  rusgrnumwwlks  29495  clwwlkwwlksb  29574  clwwlknwwlksnb  29575  dmdmd  31820  nfpconfp  32123  funcnvmpt  32159  1stpreimas  32194  xrdifh  32258  swrdrn3  32386  lsmsnorb  32775  ghmqusker  32806  rhmpreimacnlem  33162  ismntop  33304  eulerpartlemgh  33675  signslema  33871  fmlafvel  34674  topdifinfindis  36530  leceifl  36780  lindsadd  36784  lindsenlbs  36786  iblabsnclem  36854  ftc1anclem6  36869  areacirclem5  36883  areacirc  36884  brcoss3  37606  lsatfixedN  38182  cdlemg10c  39813  diaglbN  40229  dih1  40460  dihglbcpreN  40474  mapdcv  40834  dvdsexpnn0  41534  ellz1  41807  islssfg  42114  proot1ex  42245  tfsconcat00  42399  eliooshift  44517  clim2cf  44664  dfatdmfcoafv2  46260  sfprmdvdsmersenne  46569  odd2np1ALTV  46640  rrx2plordisom  47496  i0oii  47639  io1ii  47640