Theorem 3bitr4rd 315

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  inimasn  6145  funcnvmpt  6996  isof1oidb  7333  oacan  8560  ecdmn0  8774  wemapwe  9702  ttrclselem2  9731  r1pw  9863  adderpqlem  11043  mulerpqlem  11044  lterpq  11059  ltanq  11060  genpass  11098  readdcan  11488  lemuldiv  12201  msq11  12222  avglt2  12589  qbtwnre  13333  iooshf  13561  swrdrn3  14807  clim2c  15678  lo1o1  15705  climabs0  15758  reef11  16293  absefib  16372  efieq1re  16373  nndivides  16438  oddnn02np1  16524  oddge22np1  16525  evennn02n  16526  evennn2n  16527  halfleoddlt  16538  pc2dvds  17063  pcmpt  17076  subsubc  18034  ghmqusker  19507  odmulgid  19774  gexdvds  19804  submcmn2  20059  obslbs  22042  lindsenlbs  22163  cnntr  23599  cndis  23615  cnindis  23616  cnpdis  23617  lmres  23624  cmpfi  23732  ist0-4  24054  txhmeo  24128  tsmssubm  24468  blin  24746  cncfmet  25236  icopnfcnv  25269  lmmbrf  25589  iscauf  25607  causs  25625  mbfposr  25979  itg2gt0  26087  limcflf  26207  limcres  26212  lhop1  26340  dvdsr1p  26488  fsumvma2  27547  vmasum  27549  chpchtsum  27552  bposlem1  27617  addscan2  28385  lesubaddsd  28485  mulscan2dlem  28570  bdayfinbndlem1  28859  iscgrgd  28982  tgcgr4  29000  lnrot1  29097  dfprlng2  29431  eqeelen  29488  nbusgreledg  29940  nb3grprlem2  29968  wspthsnwspthsnon  30511  rusgrnumwwlks  30572  clwwlkwwlksb  30651  clwwlknwwlksnb  30652  dmdmd  32908  nfpconfp  33274  1stpreimas  33347  xrdifh  33419  lsmsnorb  33993  esplyfval1  34252  fldextrspunlsp  34353  rhmpreimacnlem  34563  ismntop  34705  eulerpartlemgh  35057  signslema  35238  fmlafvel  36237  topdifinfindis  38363  leceifl  38626  lindsadd  38630  iblabsnclem  38695  ftc1anclem6  38710  areacirclem5  38724  areacirc  38725  brcoss3  39549  lsatfixedN  40160  cdlemg10c  41790  diaglbN  42206  dih1  42437  dihglbcpreN  42451  mapdcv  42811  dvdsexpnn0  43480  ef11d  43484  ellz1  43872  islssfg  44166  proot1ex  44292  tfsconcat00  44443  eliooshift  46612  clim2cf  46754  dfatdmfcoafv2  48418  sfprmdvdsmersenne  48782  odd2np1ALTV  48866  vopnbgrelself  49047  rrx2plordisom  49930  i0oii  50128  io1ii  50129  oppccic  50252  uptrlem3  50422  uptr2  50431