Theorem 3bitr2d 307

Description: Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)

Hypotheses

Ref	Expression
3bitr2d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
3bitr2d.2	⊢ (𝜑 → (𝜃 ↔ 𝜒))
3bitr2d.3	⊢ (𝜑 → (𝜃 ↔ 𝜏))

Assertion

Ref	Expression
3bitr2d	⊢ (𝜑 → (𝜓 ↔ 𝜏))

Proof of Theorem 3bitr2d

Step	Hyp	Ref	Expression
1		3bitr2d.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		3bitr2d.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
3	1, 2	bitr4d 282	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4		3bitr2d.3	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
5	3, 4	bitrd 279	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:  raltpd  4748  opiota  8041  mapsnend  9010  adderpqlem  10914  mulerpqlem  10915  lesub2  11680  rec11  11887  fimaxre  12134  fiminre  12137  avglt1  12427  ixxun  13329  modmuladdnn0  13887  hashdom  14351  hashle00  14372  hashf1lem1  14427  swrdspsleq  14637  repsdf2  14750  2shfti  15053  mulre  15094  rlim  15468  rlim2  15469  modremain  16385  nn0seqcvgd  16547  divgcdcoprm0  16642  prmreclem6  16899  pwsleval  17463  issubc  17804  ismgmid  18599  grpsubeq0  18965  grpsubadd  18967  eqg0el  19122  gastacos  19249  orbsta  19252  lsslss  20874  prmirredlem  21389  zndvds  21466  zntoslem  21473  cygznlem1  21483  islindf2  21730  ismhp3  22036  coe1mul2lem1  22160  ply1chr  22200  restcld  23066  leordtvallem1  23104  leordtvallem2  23105  ist1-2  23241  xkoccn  23513  qtopcld  23607  ordthmeolem  23695  qustgpopn  24014  isxmet2d  24222  prdsxmetlem  24263  xblss2  24297  imasf1oxms  24384  neibl  24396  xrtgioo  24702  xrsxmet  24705  isncvsngp  25056  minveclem4  25339  minveclem6  25341  minveclem7  25342  mbfmulc2lem  25555  mbfmax  25557  mbfi1fseqlem4  25626  itg2gt0  25668  itg2cnlem2  25670  iblpos  25701  r1pid2  26074  logbgt0b  26710  angrteqvd  26723  affineequiv  26740  affineequiv2  26741  dcubic  26763  rlimcnp  26882  rlimcnp2  26883  efexple  27199  bposlem7  27208  lgsabs1  27254  lgsquadlem1  27298  m1lgs  27306  subadds  27981  lnhl  28549  colinearalg  28844  axcontlem2  28899  nbupgrel  29279  nb3grpr  29316  usgr0edg0rusgr  29510  isspthonpth  29686  rusgrnumwwlkl1  29905  eupth2lem3lem4  30167  minvecolem4  30816  minvecolem6  30818  minvecolem7  30819  hvmulcan2  31009  xppreima  32576  fzo0opth  32735  fracerl  33263  dvdsrspss  33365  ply1degltel  33567  r1pid2OLD  33581  smatrcl  33793  pstmxmet  33894  xrge0iifcnv  33930  ballotlemsima  34514  poimirlem27  37648  itg2addnclem  37672  itg2addnclem2  37673  iblabsnclem  37684  areacirclem2  37710  areacirclem4  37712  cvlcvrp  39340  ontric3g  43518  alephiso2  43554  sqrtcvallem1  43627  ntrclsk2  44064  ntrclsk13  44067  ntrneixb  44091  neicvgel1  44115  radcnvrat  44310  limsupmnflem  45725  dfvopnbgr2  47857  pgnbgreunbgrlem2lem1  48108  pgnbgreunbgrlem2lem2  48109  logbge0b  48556  affinecomb2  48696  line2x  48747  itscnhlc0yqe  48752