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  6162  funcnvmpt  7024  isof1oidb  7361  oacan  8592  ecdmn0  8806  wemapwe  9733  ttrclselem2  9762  r1pw  9894  adderpqlem  11076  mulerpqlem  11077  lterpq  11092  ltanq  11093  genpass  11131  readdcan  11521  lemuldiv  12235  msq11  12256  avglt2  12623  qbtwnre  13367  iooshf  13595  swrdrn3  14842  clim2c  15713  lo1o1  15740  climabs0  15793  reef11  16328  absefib  16407  efieq1re  16408  nndivides  16473  oddnn02np1  16559  oddge22np1  16560  evennn02n  16561  evennn2n  16562  halfleoddlt  16573  pc2dvds  17098  pcmpt  17111  subsubc  18069  ghmqusker  19543  odmulgid  19810  gexdvds  19840  submcmn2  20095  obslbs  22080  lindsenlbs  22201  cnntr  23637  cndis  23653  cnindis  23654  cnpdis  23655  lmres  23662  cmpfi  23770  ist0-4  24092  txhmeo  24166  tsmssubm  24506  blin  24784  cncfmet  25274  icopnfcnv  25307  lmmbrf  25627  iscauf  25645  causs  25663  mbfposr  26017  itg2gt0  26125  limcflf  26245  limcres  26250  lhop1  26378  dvdsr1p  26526  fsumvma2  27587  vmasum  27589  chpchtsum  27592  bposlem1  27657  addscan2  28425  lesubaddsd  28525  mulscan2dlem  28610  bdayfinbndlem1  28899  iscgrgd  29022  tgcgr4  29040  lnrot1  29137  dfprlng2  29471  eqeelen  29528  nbusgreledg  29980  nb3grprlem2  30008  wspthsnwspthsnon  30551  rusgrnumwwlks  30612  clwwlkwwlksb  30691  clwwlknwwlksnb  30692  dmdmd  32948  nfpconfp  33314  1stpreimas  33386  xrdifh  33458  lsmsnorb  34043  esplyfval1  34309  fldextrspunlsp  34410  rhmpreimacnlem  34620  ismntop  34762  eulerpartlemgh  35114  signslema  35295  fmlafvel  36351  topdifinfindis  38530  leceifl  38793  lindsadd  38797  iblabsnclem  38862  ftc1anclem6  38877  areacirclem5  38891  areacirc  38892  brcoss3  39714  lsatfixedN  40325  cdlemg10c  41955  diaglbN  42371  dih1  42602  dihglbcpreN  42616  mapdcv  42976  dvdsexpnn0  43646  ef11d  43650  ellz1  44038  islssfg  44332  proot1ex  44453  tfsconcat00  44604  eliooshift  46785  clim2cf  46927  dfatdmfcoafv2  48591  sfprmdvdsmersenne  48955  odd2np1ALTV  49039  vopnbgrelself  49220  rrx2plordisom  50161  i0oii  50359  io1ii  50360  oppccic  50483  uptrlem3  50653  uptr2  50662