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  5927  fndmdif  7017  weniso  7332  sbcopeq1a  8031  xpord2pred  8127  snmapen  9012  dmttrcl  9681  cfss  10225  posdif  11678  lesub1  11679  lesub0  11702  possumd  11810  ltdivmul  12065  ledivmul  12066  zlem1lt  12592  zltlem1  12593  negelrp  12993  ioon0  13339  fzn  13508  fzrev2  13556  fz1sbc  13568  elfzp1b  13569  sumsqeq0  14151  fz1isolem  14433  sqrtle  15233  absgt0  15298  isershft  15637  incexc2  15811  dvdssubr  16282  gcdn0gt0  16495  divgcdcoprmex  16643  pcfac  16877  ramval  16986  isrnghm  20357  iunocv  21597  ltbwe  21958  lmbrf  23154  perfcls  23259  ovolscalem1  25421  itg2mulclem  25654  sineq0  26440  efif1olem4  26461  logge0b  26547  loggt0b  26548  logle1b  26549  loglt1b  26550  atanord  26844  rlimcnp2  26883  bposlem7  27208  lgsprme0  27257  rpvmasum2  27430  sltsubsub2bd  27995  posdifsd  28008  sltmuldivwd  28111  pw2gt0divsd  28335  pw2ge0divsd  28336  trgcgrg  28449  legov3  28532  opphllem6  28686  ebtwntg  28916  wwlksm1edg  29818  clwlkclwwlk2  29939  hial2eq2  31043  adjsym  31769  cnvadj  31828  eigvalcl  31897  mddmd  32237  mdslmd2i  32266  elat2  32276  indpreima  32795  xdivpnfrp  32860  isorng  33284  ply1dg1rt  33555  unitdivcld  33898  ioosconn  35241  poimirlem26  37647  areacirclem1  37709  isat3  39307  ishlat3N  39354  cvrval5  39416  llnexchb2  39870  lhpoc2N  40016  lhprelat3N  40041  lautcnvle  40090  lautcvr  40093  ltrncnvatb  40139  cdlemb3  40607  cdlemg17h  40669  dih0vbN  41283  djhcvat42  41416  dvh4dimat  41439  mapdordlem2  41638  aks6d1c5lem1  42131  f1o2d2  42228  eluzp1  42302  reltsub1  42381  reltsubadd2  42382  sn-ltmul2d  42468  fsuppind  42585  diophun  42768  jm2.19lem4  42988  ordeldifsucon  43255  orddif0suc  43264  uneqsn  44021  xrralrecnnge  45393  limsupre2lem  45729  modmkpkne  47366  prprelb  47521  flsqrt5  47599  lincfsuppcl  48406