Theorem 3bitr4rd 313

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

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  snssg  4630  inimasn  5896  isof1oidb  6947  oacan  8031  ecdmn0  8193  wemapwe  9013  r1pw  9127  adderpqlem  10229  mulerpqlem  10230  lterpq  10245  ltanq  10246  genpass  10284  readdcan  10667  lemuldiv  11374  msq11  11395  avglt2  11730  qbtwnre  12446  iooshf  12669  clim2c  14700  lo1o1  14727  climabs0  14780  reef11  15309  absefib  15388  efieq1re  15389  nndivides  15454  oddnn02np1  15534  oddge22np1  15535  evennn02n  15536  evennn2n  15537  halfleoddlt  15548  pc2dvds  16048  pcmpt  16061  subsubc  16956  odmulgid  18415  gexdvds  18443  submcmn2  18688  obslbs  20560  cnntr  21571  cndis  21587  cnindis  21588  cnpdis  21589  lmres  21596  cmpfi  21704  ist0-4  22025  txhmeo  22099  tsmssubm  22438  blin  22718  cncfmet  23203  icopnfcnv  23233  lmmbrf  23552  iscauf  23570  causs  23588  mbfposr  23940  itg2gt0  24048  limcflf  24166  limcres  24171  lhop1  24298  dvdsr1p  24442  fsumvma2  25476  vmasum  25478  chpchtsum  25481  bposlem1  25546  iscgrgd  25985  tgcgr4  26003  lnrot1  26095  eqeelen  26377  nbusgreledg  26822  nb3grprlem2  26850  wspthsnwspthsnon  27381  rusgrnumwwlks  27439  clwlkclwwlk2  27467  clwwlkwwlksb  27519  clwwlknwwlksnb  27520  clwwlknonwwlknonb  27571  dmdmd  29764  nfpconfp  30063  funcnvmpt  30098  1stpreimas  30125  xrdifh  30187  ismntop  30880  eulerpartlemgh  31249  signslema  31445  fmlafvel  32242  topdifinfindis  34179  leceifl  34433  lindsadd  34437  lindsenlbs  34439  iblabsnclem  34507  ftc1anclem6  34524  areacirclem5  34538  areacirc  34539  brcoss3  35230  lsatfixedN  35697  cdlemg10c  37327  diaglbN  37743  dih1  37974  dihglbcpreN  37988  mapdcv  38348  ellz1  38870  islssfg  39176  proot1ex  39307  eliooshift  41345  clim2cf  41494  dfatdmfcoafv2  42991  sfprmdvdsmersenne  43272  odd2np1ALTV  43343  rrx2plordisom  44213