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  4738  inimasn  6109  isof1oidb  7265  oacan  8473  ecdmn0  8684  wemapwe  9612  ttrclselem2  9641  r1pw  9760  adderpqlem  10867  mulerpqlem  10868  lterpq  10883  ltanq  10884  genpass  10922  readdcan  11308  lemuldiv  12023  msq11  12044  avglt2  12381  qbtwnre  13119  iooshf  13347  clim2c  15430  lo1o1  15457  climabs0  15510  reef11  16046  absefib  16125  efieq1re  16126  nndivides  16191  oddnn02np1  16277  oddge22np1  16278  evennn02n  16279  evennn2n  16280  halfleoddlt  16291  pc2dvds  16809  pcmpt  16822  subsubc  17778  ghmqusker  19184  odmulgid  19451  gexdvds  19481  submcmn2  19736  obslbs  21655  cnntr  23178  cndis  23194  cnindis  23195  cnpdis  23196  lmres  23203  cmpfi  23311  ist0-4  23632  txhmeo  23706  tsmssubm  24046  blin  24325  cncfmet  24818  icopnfcnv  24856  lmmbrf  25178  iscauf  25196  causs  25214  mbfposr  25569  itg2gt0  25677  limcflf  25798  limcres  25803  lhop1  25935  dvdsr1p  26085  fsumvma2  27141  vmasum  27143  chpchtsum  27146  bposlem1  27211  addscan2  27923  slesubaddd  28020  mulscan2dlem  28104  iscgrgd  28476  tgcgr4  28494  lnrot1  28586  eqeelen  28867  nbusgreledg  29316  nb3grprlem2  29344  wspthsnwspthsnon  29879  rusgrnumwwlks  29937  clwwlkwwlksb  30016  clwwlknwwlksnb  30017  dmdmd  32262  nfpconfp  32589  funcnvmpt  32624  1stpreimas  32662  xrdifh  32736  swrdrn3  32910  lsmsnorb  33341  fldextrspunlsp  33648  rhmpreimacnlem  33853  ismntop  33995  eulerpartlemgh  34348  signslema  34532  fmlafvel  35360  topdifinfindis  37322  leceifl  37591  lindsadd  37595  lindsenlbs  37597  iblabsnclem  37665  ftc1anclem6  37680  areacirclem5  37694  areacirc  37695  brcoss3  38412  lsatfixedN  38990  cdlemg10c  40621  diaglbN  41037  dih1  41268  dihglbcpreN  41282  mapdcv  41642  dvdsexpnn0  42310  ef11d  42315  ellz1  42743  islssfg  43046  proot1ex  43172  tfsconcat00  43323  eliooshift  45491  clim2cf  45635  dfatdmfcoafv2  47242  sfprmdvdsmersenne  47591  odd2np1ALTV  47662  vopnbgrelself  47843  rrx2plordisom  48712  i0oii  48908  io1ii  48909  oppccic  49033  uptrlem3  49201  uptr2  49210