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:  snssg  4715  inimasn  6048  isof1oidb  7175  oacan  8341  ecdmn0  8503  wemapwe  9385  r1pw  9534  adderpqlem  10641  mulerpqlem  10642  lterpq  10657  ltanq  10658  genpass  10696  readdcan  11079  lemuldiv  11785  msq11  11806  avglt2  12142  qbtwnre  12862  iooshf  13087  clim2c  15142  lo1o1  15169  climabs0  15222  reef11  15756  absefib  15835  efieq1re  15836  nndivides  15901  oddnn02np1  15985  oddge22np1  15986  evennn02n  15987  evennn2n  15988  halfleoddlt  15999  pc2dvds  16508  pcmpt  16521  subsubc  17484  odmulgid  19076  gexdvds  19104  submcmn2  19355  obslbs  20847  cnntr  22334  cndis  22350  cnindis  22351  cnpdis  22352  lmres  22359  cmpfi  22467  ist0-4  22788  txhmeo  22862  tsmssubm  23202  blin  23482  cncfmet  23978  icopnfcnv  24011  lmmbrf  24331  iscauf  24349  causs  24367  mbfposr  24721  itg2gt0  24830  limcflf  24950  limcres  24955  lhop1  25083  dvdsr1p  25231  fsumvma2  26267  vmasum  26269  chpchtsum  26272  bposlem1  26337  iscgrgd  26778  tgcgr4  26796  lnrot1  26888  eqeelen  27175  nbusgreledg  27623  nb3grprlem2  27651  wspthsnwspthsnon  28182  rusgrnumwwlks  28240  clwwlkwwlksb  28319  clwwlknwwlksnb  28320  dmdmd  30563  nfpconfp  30868  funcnvmpt  30906  1stpreimas  30940  xrdifh  31003  swrdrn3  31129  lsmsnorb  31481  rhmpreimacnlem  31736  ismntop  31876  eulerpartlemgh  32245  signslema  32441  fmlafvel  33247  ttrclselem2  33712  topdifinfindis  35444  leceifl  35693  lindsadd  35697  lindsenlbs  35699  iblabsnclem  35767  ftc1anclem6  35782  areacirclem5  35796  areacirc  35797  brcoss3  36483  lsatfixedN  36950  cdlemg10c  38580  diaglbN  38996  dih1  39227  dihglbcpreN  39241  mapdcv  39601  dvdsexpnn0  40262  ellz1  40505  islssfg  40811  proot1ex  40942  eliooshift  42934  clim2cf  43081  dfatdmfcoafv2  44633  sfprmdvdsmersenne  44943  odd2np1ALTV  45014  rrx2plordisom  45957  i0oii  46101  io1ii  46102