Theorem 3bitr4rd 303

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

Syntax hints:   → wi 4   ↔ wb 197

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 198

This theorem is referenced by:  snssg  4469  inimasn  5733  isof1oidb  6766  oacan  7833  ecdmn0  7992  wemapwe  8809  r1pw  8923  adderpqlem  10029  mulerpqlem  10030  lterpq  10045  ltanq  10046  genpass  10084  readdcan  10464  lemuldiv  11157  msq11  11178  avglt2  11517  qbtwnre  12232  iooshf  12454  clim2c  14521  lo1o1  14548  climabs0  14601  reef11  15131  absefib  15210  efieq1re  15211  nndivides  15275  oddnn02np1  15354  oddge22np1  15355  evennn02n  15356  evennn2n  15357  halfleoddlt  15368  pc2dvds  15862  pcmpt  15875  subsubc  16778  odmulgid  18235  gexdvds  18263  submcmn2  18510  obslbs  20350  cnntr  21359  cndis  21375  cnindis  21376  cnpdis  21377  lmres  21384  cmpfi  21491  ist0-4  21812  txhmeo  21886  tsmssubm  22225  blin  22505  cncfmet  22990  icopnfcnv  23020  lmmbrf  23339  iscauf  23357  causs  23375  mbfposr  23710  itg2gt0  23818  limcflf  23936  limcres  23941  lhop1  24068  dvdsr1p  24212  fsumvma2  25230  vmasum  25232  chpchtsum  25235  bposlem1  25300  iscgrgd  25699  tgcgr4  25717  lnrot1  25809  eqeelen  26075  nbusgreledg  26528  nb3grprlem2  26562  wspthsnwspthsnon  27137  wspthsnwspthsnonOLD  27139  rusgrnumwwlks  27199  rusgrnumwwlksOLD  27200  clwlkclwwlk2  27231  clwlkclwwlk2OLD  27232  clwwlkwwlksb  27304  clwwlknwwlksnb  27305  clwwlknonwwlknonb  27379  clwwlknonwwlknonbOLD  27380  dmdmd  29615  funcnvmpt  29917  1stpreimas  29932  xrdifh  29991  ismntop  30517  eulerpartlemgh  30887  signslema  31088  topdifinfindis  33627  leceifl  33822  lindsenlbs  33828  iblabsnclem  33896  ftc1anclem6  33913  areacirclem5  33927  areacirc  33928  brcoss3  34617  lsatfixedN  34965  cdlemg10c  36595  diaglbN  37011  dih1  37242  dihglbcpreN  37256  mapdcv  37616  ellz1  38008  islssfg  38317  proot1ex  38456  eliooshift  40371  clim2cf  40520  dfatdmfcoafv2  42002  sfprmdvdsmersenne  42196  odd2np1ALTV  42261