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  6146  funcnvmpt  6993  isof1oidb  7330  oacan  8549  ecdmn0  8763  wemapwe  9691  ttrclselem2  9720  r1pw  9852  adderpqlem  11032  mulerpqlem  11033  lterpq  11048  ltanq  11049  genpass  11087  readdcan  11477  lemuldiv  12190  msq11  12211  avglt2  12578  qbtwnre  13322  iooshf  13550  swrdrn3  14795  clim2c  15665  lo1o1  15692  climabs0  15745  reef11  16280  absefib  16359  efieq1re  16360  nndivides  16425  oddnn02np1  16511  oddge22np1  16512  evennn02n  16513  evennn2n  16514  halfleoddlt  16525  pc2dvds  17050  pcmpt  17063  subsubc  18021  ghmqusker  19494  odmulgid  19761  gexdvds  19791  submcmn2  20046  obslbs  22029  lindsenlbs  22150  cnntr  23586  cndis  23602  cnindis  23603  cnpdis  23604  lmres  23611  cmpfi  23719  ist0-4  24041  txhmeo  24115  tsmssubm  24455  blin  24733  cncfmet  25223  icopnfcnv  25256  lmmbrf  25576  iscauf  25594  causs  25612  mbfposr  25966  itg2gt0  26074  limcflf  26194  limcres  26199  lhop1  26327  dvdsr1p  26475  fsumvma2  27534  vmasum  27536  chpchtsum  27539  bposlem1  27604  addscan2  28372  lesubaddsd  28472  mulscan2dlem  28557  bdayfinbndlem1  28846  iscgrgd  28969  tgcgr4  28987  lnrot1  29084  dfprlng2  29418  eqeelen  29475  nbusgreledg  29927  nb3grprlem2  29955  wspthsnwspthsnon  30498  rusgrnumwwlks  30559  clwwlkwwlksb  30638  clwwlknwwlksnb  30639  dmdmd  32895  nfpconfp  33219  1stpreimas  33292  xrdifh  33365  lsmsnorb  33939  esplyfval1  34198  fldextrspunlsp  34299  rhmpreimacnlem  34509  ismntop  34651  eulerpartlemgh  35003  signslema  35184  fmlafvel  36129  topdifinfindis  38249  leceifl  38512  lindsadd  38516  iblabsnclem  38581  ftc1anclem6  38596  areacirclem5  38610  areacirc  38611  brcoss3  39435  lsatfixedN  40046  cdlemg10c  41676  diaglbN  42092  dih1  42323  dihglbcpreN  42337  mapdcv  42697  dvdsexpnn0  43366  ef11d  43370  ellz1  43757  islssfg  44056  proot1ex  44182  tfsconcat00  44333  eliooshift  46487  clim2cf  46629  dfatdmfcoafv2  48293  sfprmdvdsmersenne  48657  odd2np1ALTV  48741  vopnbgrelself  48922  rrx2plordisom  49804  i0oii  49997  io1ii  49998  oppccic  50121  uptrlem3  50289  uptr2  50298