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  2254  elrnmpt1  5940  fndmdif  7032  weniso  7347  sbcopeq1a  8048  xpord2pred  8144  snmapen  9052  dmttrcl  9735  cfss  10279  posdif  11730  lesub1  11731  lesub0  11754  possumd  11862  ltdivmul  12117  ledivmul  12118  zlem1lt  12644  zltlem1  12645  negelrp  13042  ioon0  13388  fzn  13557  fzrev2  13605  fz1sbc  13617  elfzp1b  13618  sumsqeq0  14197  fz1isolem  14479  sqrtle  15279  absgt0  15343  isershft  15680  incexc2  15854  dvdssubr  16324  gcdn0gt0  16537  divgcdcoprmex  16685  pcfac  16919  ramval  17028  isrnghm  20401  iunocv  21641  ltbwe  22002  lmbrf  23198  perfcls  23303  ovolscalem1  25466  itg2mulclem  25699  sineq0  26485  efif1olem4  26506  logge0b  26592  loggt0b  26593  logle1b  26594  loglt1b  26595  atanord  26889  rlimcnp2  26928  bposlem7  27253  lgsprme0  27302  rpvmasum2  27475  sltsubsub2bd  28040  posdifsd  28053  sltmuldivwd  28156  pw2gt0divsd  28380  pw2ge0divsd  28381  trgcgrg  28494  legov3  28577  opphllem6  28731  ebtwntg  28961  wwlksm1edg  29863  clwlkclwwlk2  29984  hial2eq2  31088  adjsym  31814  cnvadj  31873  eigvalcl  31942  mddmd  32282  mdslmd2i  32311  elat2  32321  indpreima  32842  xdivpnfrp  32907  isorng  33321  ply1dg1rt  33592  unitdivcld  33932  ioosconn  35269  poimirlem26  37670  areacirclem1  37732  isat3  39325  ishlat3N  39372  cvrval5  39434  llnexchb2  39888  lhpoc2N  40034  lhprelat3N  40059  lautcnvle  40108  lautcvr  40111  ltrncnvatb  40157  cdlemb3  40625  cdlemg17h  40687  dih0vbN  41301  djhcvat42  41434  dvh4dimat  41457  mapdordlem2  41656  aks6d1c5lem1  42149  f1o2d2  42284  eluzp1  42356  reltsub1  42429  reltsubadd2  42430  sn-ltmul2d  42504  fsuppind  42613  diophun  42796  jm2.19lem4  43016  ordeldifsucon  43283  orddif0suc  43292  uneqsn  44049  xrralrecnnge  45417  limsupre2lem  45753  prprelb  47530  flsqrt5  47608  lincfsuppcl  48389