Theorem bitr2d 280

Description: Deduction form of bitr2i 276. (Contributed by NM, 9-Jun-2004.)

Hypotheses

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

Assertion

Ref	Expression
bitr2d	⊢ (𝜑 → (𝜃 ↔ 𝜓))

Proof of Theorem bitr2d

Step	Hyp	Ref	Expression
1		bitr2d.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		bitr2d.2	. . 3 ⊢ (𝜑 → (𝜒 ↔ 𝜃))
3	1, 2	bitrd 279	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4	3	bicomd 223	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:  3bitrrd  306  3bitr2rd  308  pm5.18  381  ifptru  1074  sbequ12a  2255  elrnmpt1  5924  fndmdif  7014  weniso  7329  sbcopeq1a  8028  xpord2pred  8124  snmapen  9009  dmttrcl  9674  cfss  10218  posdif  11671  lesub1  11672  lesub0  11695  possumd  11803  ltdivmul  12058  ledivmul  12059  zlem1lt  12585  zltlem1  12586  negelrp  12986  ioon0  13332  fzn  13501  fzrev2  13549  fz1sbc  13561  elfzp1b  13562  sumsqeq0  14144  fz1isolem  14426  sqrtle  15226  absgt0  15291  isershft  15630  incexc2  15804  dvdssubr  16275  gcdn0gt0  16488  divgcdcoprmex  16636  pcfac  16870  ramval  16979  isrnghm  20350  iunocv  21590  ltbwe  21951  lmbrf  23147  perfcls  23252  ovolscalem1  25414  itg2mulclem  25647  sineq0  26433  efif1olem4  26454  logge0b  26540  loggt0b  26541  logle1b  26542  loglt1b  26543  atanord  26837  rlimcnp2  26876  bposlem7  27201  lgsprme0  27250  rpvmasum2  27423  sltsubsub2bd  27988  posdifsd  28001  sltmuldivwd  28104  pw2gt0divsd  28328  pw2ge0divsd  28329  trgcgrg  28442  legov3  28525  opphllem6  28679  ebtwntg  28909  wwlksm1edg  29811  clwlkclwwlk2  29932  hial2eq2  31036  adjsym  31762  cnvadj  31821  eigvalcl  31890  mddmd  32230  mdslmd2i  32259  elat2  32269  indpreima  32788  xdivpnfrp  32853  isorng  33277  ply1dg1rt  33548  unitdivcld  33891  ioosconn  35234  poimirlem26  37640  areacirclem1  37702  isat3  39300  ishlat3N  39347  cvrval5  39409  llnexchb2  39863  lhpoc2N  40009  lhprelat3N  40034  lautcnvle  40083  lautcvr  40086  ltrncnvatb  40132  cdlemb3  40600  cdlemg17h  40662  dih0vbN  41276  djhcvat42  41409  dvh4dimat  41432  mapdordlem2  41631  aks6d1c5lem1  42124  f1o2d2  42221  eluzp1  42295  reltsub1  42374  reltsubadd2  42375  sn-ltmul2d  42461  fsuppind  42578  diophun  42761  jm2.19lem4  42981  ordeldifsucon  43248  orddif0suc  43257  uneqsn  44014  xrralrecnnge  45386  limsupre2lem  45722  modmkpkne  47362  prprelb  47517  flsqrt5  47595  lincfsuppcl  48402