Theorem 3bitr4rd 311

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  snssgOLD  4728  inimasn  6079  isof1oidb  7232  oacan  8425  ecdmn0  8591  wemapwe  9523  ttrclselem2  9552  r1pw  9671  adderpqlem  10780  mulerpqlem  10781  lterpq  10796  ltanq  10797  genpass  10835  readdcan  11219  lemuldiv  11925  msq11  11946  avglt2  12282  qbtwnre  13003  iooshf  13228  clim2c  15283  lo1o1  15310  climabs0  15363  reef11  15897  absefib  15976  efieq1re  15977  nndivides  16042  oddnn02np1  16126  oddge22np1  16127  evennn02n  16128  evennn2n  16129  halfleoddlt  16140  pc2dvds  16647  pcmpt  16660  subsubc  17635  odmulgid  19228  gexdvds  19256  submcmn2  19507  obslbs  21008  cnntr  22497  cndis  22513  cnindis  22514  cnpdis  22515  lmres  22522  cmpfi  22630  ist0-4  22951  txhmeo  23025  tsmssubm  23365  blin  23645  cncfmet  24143  icopnfcnv  24176  lmmbrf  24497  iscauf  24515  causs  24533  mbfposr  24887  itg2gt0  24996  limcflf  25116  limcres  25121  lhop1  25249  dvdsr1p  25397  fsumvma2  26433  vmasum  26435  chpchtsum  26438  bposlem1  26503  iscgrgd  26982  tgcgr4  27000  lnrot1  27092  eqeelen  27380  nbusgreledg  27828  nb3grprlem2  27856  wspthsnwspthsnon  28389  rusgrnumwwlks  28447  clwwlkwwlksb  28526  clwwlknwwlksnb  28527  dmdmd  30770  nfpconfp  31075  funcnvmpt  31112  1stpreimas  31146  xrdifh  31209  swrdrn3  31335  lsmsnorb  31684  rhmpreimacnlem  31940  ismntop  32082  eulerpartlemgh  32451  signslema  32647  fmlafvel  33453  topdifinfindis  35577  leceifl  35826  lindsadd  35830  lindsenlbs  35832  iblabsnclem  35900  ftc1anclem6  35915  areacirclem5  35929  areacirc  35930  brcoss3  36659  lsatfixedN  37235  cdlemg10c  38865  diaglbN  39281  dih1  39512  dihglbcpreN  39526  mapdcv  39886  dvdsexpnn0  40551  ellz1  40799  islssfg  41106  proot1ex  41237  eliooshift  43288  clim2cf  43435  dfatdmfcoafv2  45005  sfprmdvdsmersenne  45314  odd2np1ALTV  45385  rrx2plordisom  46328  i0oii  46472  io1ii  46473