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:  inimasn  6114  funcnvmpt  6943  isof1oidb  7272  oacan  8476  ecdmn0  8689  wemapwe  9609  ttrclselem2  9638  r1pw  9760  adderpqlem  10868  mulerpqlem  10869  lterpq  10884  ltanq  10885  genpass  10923  readdcan  11311  lemuldiv  12027  msq11  12048  avglt2  12407  qbtwnre  13142  iooshf  13370  clim2c  15458  lo1o1  15485  climabs0  15538  reef11  16077  absefib  16156  efieq1re  16157  nndivides  16222  oddnn02np1  16308  oddge22np1  16309  evennn02n  16310  evennn2n  16311  halfleoddlt  16322  pc2dvds  16841  pcmpt  16854  subsubc  17811  ghmqusker  19253  odmulgid  19520  gexdvds  19550  submcmn2  19805  obslbs  21720  cnntr  23250  cndis  23266  cnindis  23267  cnpdis  23268  lmres  23275  cmpfi  23383  ist0-4  23704  txhmeo  23778  tsmssubm  24118  blin  24396  cncfmet  24886  icopnfcnv  24919  lmmbrf  25239  iscauf  25257  causs  25275  mbfposr  25629  itg2gt0  25737  limcflf  25858  limcres  25863  lhop1  25991  dvdsr1p  26139  fsumvma2  27191  vmasum  27193  chpchtsum  27196  bposlem1  27261  addscan2  27999  lesubaddsd  28099  mulscan2dlem  28184  bdayfinbndlem1  28473  iscgrgd  28595  tgcgr4  28613  lnrot1  28705  eqeelen  28987  nbusgreledg  29436  nb3grprlem2  29464  wspthsnwspthsnon  29999  rusgrnumwwlks  30060  clwwlkwwlksb  30139  clwwlknwwlksnb  30140  dmdmd  32386  nfpconfp  32720  1stpreimas  32794  xrdifh  32868  swrdrn3  33030  lsmsnorb  33466  esplyfval1  33732  fldextrspunlsp  33834  rhmpreimacnlem  34044  ismntop  34186  eulerpartlemgh  34538  signslema  34722  fmlafvel  35583  topdifinfindis  37676  leceifl  37944  lindsadd  37948  lindsenlbs  37950  iblabsnclem  38018  ftc1anclem6  38033  areacirclem5  38047  areacirc  38048  brcoss3  38858  lsatfixedN  39469  cdlemg10c  41099  diaglbN  41515  dih1  41746  dihglbcpreN  41760  mapdcv  42120  dvdsexpnn0  42780  ef11d  42785  ellz1  43213  islssfg  43516  proot1ex  43642  tfsconcat00  43793  eliooshift  45954  clim2cf  46096  dfatdmfcoafv2  47714  sfprmdvdsmersenne  48078  odd2np1ALTV  48162  vopnbgrelself  48343  rrx2plordisom  49211  i0oii  49407  io1ii  49408  oppccic  49531  uptrlem3  49699  uptr2  49708