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  2251  elrnmpt1  5973  fndmdif  7061  weniso  7373  sbcopeq1a  8072  xpord2pred  8168  snmapen  9076  dmttrcl  9758  cfss  10302  posdif  11753  lesub1  11754  lesub0  11777  possumd  11885  ltdivmul  12140  ledivmul  12141  zlem1lt  12666  zltlem1  12667  negelrp  13065  ioon0  13409  fzn  13576  fzrev2  13624  fz1sbc  13636  elfzp1b  13637  sumsqeq0  14214  fz1isolem  14496  sqrtle  15295  absgt0  15359  isershft  15696  incexc2  15870  dvdssubr  16338  gcdn0gt0  16551  divgcdcoprmex  16699  pcfac  16932  ramval  17041  isrnghm  20457  iunocv  21716  ltbwe  22079  lmbrf  23283  perfcls  23388  ovolscalem1  25561  itg2mulclem  25795  sineq0  26580  efif1olem4  26601  logge0b  26687  loggt0b  26688  logle1b  26689  loglt1b  26690  atanord  26984  rlimcnp2  27023  bposlem7  27348  lgsprme0  27397  rpvmasum2  27570  sltsubsub2bd  28128  posdifsd  28141  sltmuldivwd  28240  trgcgrg  28537  legov3  28620  opphllem6  28774  ebtwntg  29011  wwlksm1edg  29910  clwlkclwwlk2  30031  hial2eq2  31135  adjsym  31861  cnvadj  31920  eigvalcl  31989  mddmd  32329  mdslmd2i  32358  elat2  32368  xdivpnfrp  32899  isorng  33308  ply1dg1rt  33583  unitdivcld  33861  indpreima  34005  ioosconn  35231  poimirlem26  37632  areacirclem1  37694  isat3  39288  ishlat3N  39335  cvrval5  39397  llnexchb2  39851  lhpoc2N  39997  lhprelat3N  40022  lautcnvle  40071  lautcvr  40074  ltrncnvatb  40120  cdlemb3  40588  cdlemg17h  40650  dih0vbN  41264  djhcvat42  41397  dvh4dimat  41420  mapdordlem2  41619  aks6d1c5lem1  42117  f1o2d2  42252  eluzp1  42319  reltsub1  42392  reltsubadd2  42393  sn-ltmul2d  42467  fsuppind  42576  diophun  42760  jm2.19lem4  42980  ordeldifsucon  43248  orddif0suc  43257  uneqsn  44014  xrralrecnnge  45339  limsupre2lem  45679  prprelb  47440  flsqrt5  47518  lincfsuppcl  48258