Theorem 3bitr4rd 312

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  snssgOLD  4744  inimasn  6117  isof1oidb  7281  oacan  8489  ecdmn0  8700  wemapwe  9626  ttrclselem2  9655  r1pw  9774  adderpqlem  10883  mulerpqlem  10884  lterpq  10899  ltanq  10900  genpass  10938  readdcan  11324  lemuldiv  12039  msq11  12060  avglt2  12397  qbtwnre  13135  iooshf  13363  clim2c  15447  lo1o1  15474  climabs0  15527  reef11  16063  absefib  16142  efieq1re  16143  nndivides  16208  oddnn02np1  16294  oddge22np1  16295  evennn02n  16296  evennn2n  16297  halfleoddlt  16308  pc2dvds  16826  pcmpt  16839  subsubc  17791  ghmqusker  19195  odmulgid  19460  gexdvds  19490  submcmn2  19745  obslbs  21615  cnntr  23138  cndis  23154  cnindis  23155  cnpdis  23156  lmres  23163  cmpfi  23271  ist0-4  23592  txhmeo  23666  tsmssubm  24006  blin  24285  cncfmet  24778  icopnfcnv  24816  lmmbrf  25138  iscauf  25156  causs  25174  mbfposr  25529  itg2gt0  25637  limcflf  25758  limcres  25763  lhop1  25895  dvdsr1p  26045  fsumvma2  27101  vmasum  27103  chpchtsum  27106  bposlem1  27171  addscan2  27876  slesubaddd  27973  mulscan2dlem  28057  iscgrgd  28416  tgcgr4  28434  lnrot1  28526  eqeelen  28807  nbusgreledg  29256  nb3grprlem2  29284  wspthsnwspthsnon  29819  rusgrnumwwlks  29877  clwwlkwwlksb  29956  clwwlknwwlksnb  29957  dmdmd  32202  nfpconfp  32529  funcnvmpt  32564  1stpreimas  32602  xrdifh  32676  swrdrn3  32850  lsmsnorb  33335  fldextrspunlsp  33642  rhmpreimacnlem  33847  ismntop  33989  eulerpartlemgh  34342  signslema  34526  fmlafvel  35345  topdifinfindis  37307  leceifl  37576  lindsadd  37580  lindsenlbs  37582  iblabsnclem  37650  ftc1anclem6  37665  areacirclem5  37679  areacirc  37680  brcoss3  38397  lsatfixedN  38975  cdlemg10c  40606  diaglbN  41022  dih1  41253  dihglbcpreN  41267  mapdcv  41627  dvdsexpnn0  42295  ef11d  42300  ellz1  42728  islssfg  43032  proot1ex  43158  tfsconcat00  43309  eliooshift  45477  clim2cf  45621  dfatdmfcoafv2  47228  sfprmdvdsmersenne  47577  odd2np1ALTV  47648  vopnbgrelself  47828  rrx2plordisom  48685  i0oii  48881  io1ii  48882  oppccic  49006  uptrlem3  49174  uptr2  49183