Theorem 3bitr4rd 315

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  inimasn  6147  funcnvmpt  6988  isof1oidb  7325  oacan  8535  ecdmn0  8749  wemapwe  9676  ttrclselem2  9705  r1pw  9827  adderpqlem  10963  mulerpqlem  10964  lterpq  10979  ltanq  10980  genpass  11018  readdcan  11408  lemuldiv  12119  msq11  12140  avglt2  12507  qbtwnre  13251  iooshf  13479  swrdrn3  14722  clim2c  15592  lo1o1  15619  climabs0  15672  reef11  16207  absefib  16286  efieq1re  16287  nndivides  16352  oddnn02np1  16438  oddge22np1  16439  evennn02n  16440  evennn2n  16441  halfleoddlt  16452  pc2dvds  16971  pcmpt  16984  subsubc  17942  ghmqusker  19414  odmulgid  19681  gexdvds  19711  submcmn2  19966  obslbs  21943  lindsenlbs  22064  cnntr  23500  cndis  23516  cnindis  23517  cnpdis  23518  lmres  23525  cmpfi  23633  ist0-4  23955  txhmeo  24029  tsmssubm  24369  blin  24647  cncfmet  25137  icopnfcnv  25170  lmmbrf  25490  iscauf  25508  causs  25526  mbfposr  25880  itg2gt0  25988  limcflf  26108  limcres  26113  lhop1  26241  dvdsr1p  26389  fsumvma2  27450  vmasum  27452  chpchtsum  27455  bposlem1  27520  addscan2  28258  lesubaddsd  28358  mulscan2dlem  28443  bdayfinbndlem1  28732  iscgrgd  28855  tgcgr4  28873  lnrot1  28970  dfprlng2  29304  eqeelen  29361  nbusgreledg  29813  nb3grprlem2  29841  wspthsnwspthsnon  30384  rusgrnumwwlks  30445  clwwlkwwlksb  30524  clwwlknwwlksnb  30525  dmdmd  32781  nfpconfp  33105  1stpreimas  33178  xrdifh  33251  lsmsnorb  33824  esplyfval1  34083  fldextrspunlsp  34184  rhmpreimacnlem  34394  ismntop  34536  eulerpartlemgh  34889  signslema  35070  fmlafvel  35964  topdifinfindis  38100  leceifl  38363  lindsadd  38367  iblabsnclem  38432  ftc1anclem6  38447  areacirclem5  38461  areacirc  38462  brcoss3  39271  lsatfixedN  39882  cdlemg10c  41512  diaglbN  41928  dih1  42159  dihglbcpreN  42173  mapdcv  42533  dvdsexpnn0  43209  ef11d  43214  ellz1  43612  islssfg  43911  proot1ex  44037  tfsconcat00  44188  eliooshift  46336  clim2cf  46478  dfatdmfcoafv2  48142  sfprmdvdsmersenne  48506  odd2np1ALTV  48590  vopnbgrelself  48771  rrx2plordisom  49653  i0oii  49846  io1ii  49847  oppccic  49970  uptrlem3  50138  uptr2  50147