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  6152  funcnvmpt  6991  isof1oidb  7322  oacan  8531  ecdmn0  8745  wemapwe  9664  ttrclselem2  9693  r1pw  9815  adderpqlem  10945  mulerpqlem  10946  lterpq  10961  ltanq  10962  genpass  11000  readdcan  11390  lemuldiv  12101  msq11  12122  avglt2  12489  qbtwnre  13231  iooshf  13459  clim2c  15563  lo1o1  15590  climabs0  15643  reef11  16181  absefib  16260  efieq1re  16261  nndivides  16326  oddnn02np1  16412  oddge22np1  16413  evennn02n  16414  evennn2n  16415  halfleoddlt  16426  pc2dvds  16945  pcmpt  16958  subsubc  17916  ghmqusker  19363  odmulgid  19630  gexdvds  19660  submcmn2  19915  obslbs  21891  cnntr  23443  cndis  23459  cnindis  23460  cnpdis  23461  lmres  23468  cmpfi  23576  ist0-4  23897  txhmeo  23971  tsmssubm  24311  blin  24589  cncfmet  25079  icopnfcnv  25112  lmmbrf  25432  iscauf  25450  causs  25468  mbfposr  25822  itg2gt0  25930  limcflf  26051  limcres  26056  lhop1  26184  dvdsr1p  26332  fsumvma2  27389  vmasum  27391  chpchtsum  27394  bposlem1  27459  addscan2  28197  lesubaddsd  28297  mulscan2dlem  28382  bdayfinbndlem1  28671  iscgrgd  28793  tgcgr4  28811  lnrot1  28907  dfprlng2  29208  eqeelen  29265  nbusgreledg  29714  nb3grprlem2  29742  wspthsnwspthsnon  30276  rusgrnumwwlks  30337  clwwlkwwlksb  30416  clwwlknwwlksnb  30417  dmdmd  32663  nfpconfp  32988  1stpreimas  33062  xrdifh  33136  swrdrn3  33284  lsmsnorb  33713  esplyfval1  33972  fldextrspunlsp  34073  rhmpreimacnlem  34283  ismntop  34425  eulerpartlemgh  34777  signslema  34958  fmlafvel  35885  topdifinfindis  38020  leceifl  38288  lindsadd  38292  lindsenlbs  38294  iblabsnclem  38362  ftc1anclem6  38377  areacirclem5  38391  areacirc  38392  brcoss3  39200  lsatfixedN  39811  cdlemg10c  41441  diaglbN  41857  dih1  42088  dihglbcpreN  42102  mapdcv  42462  dvdsexpnn0  43123  ef11d  43128  ellz1  43526  islssfg  43825  proot1ex  43951  tfsconcat00  44102  eliooshift  46250  clim2cf  46392  dfatdmfcoafv2  48019  sfprmdvdsmersenne  48383  odd2np1ALTV  48467  vopnbgrelself  48648  rrx2plordisom  49531  i0oii  49726  io1ii  49727  oppccic  49850  uptrlem3  50018  uptr2  50027