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 222	1 ⊢ (𝜑 → (𝜃 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  3bitrrd  306  3bitr2rd  308  pm5.18  381  ifptru  1073  sbequ12a  2239  elrnmpt1  5954  fndmdif  7045  weniso  7356  sbcopeq1a  8047  xpord2pred  8144  snmapen  9054  dmttrcl  9736  cfss  10280  posdif  11729  lesub1  11730  lesub0  11753  possumd  11861  ltdivmul  12111  ledivmul  12112  zlem1lt  12636  zltlem1  12637  negelrp  13031  ioon0  13374  fzn  13541  fzrev2  13589  fz1sbc  13601  elfzp1b  13602  sumsqeq0  14166  fz1isolem  14446  sqrtle  15231  absgt0  15295  isershft  15634  incexc2  15808  dvdssubr  16273  gcdn0gt0  16484  divgcdcoprmex  16628  prmdvdssqOLD  16681  pcfac  16859  ramval  16968  isrnghm  20369  iunocv  21600  ltbwe  21969  lmbrf  23151  perfcls  23256  ovolscalem1  25429  itg2mulclem  25663  sineq0  26445  efif1olem4  26466  logge0b  26552  loggt0b  26553  logle1b  26554  loglt1b  26555  atanord  26846  rlimcnp2  26885  bposlem7  27210  lgsprme0  27259  rpvmasum2  27432  sltsubsub2bd  27979  posdifsd  27991  sltmuldivwd  28087  trgcgrg  28306  legov3  28389  opphllem6  28543  ebtwntg  28780  wwlksm1edg  29679  clwlkclwwlk2  29800  hial2eq2  30904  adjsym  31630  cnvadj  31689  eigvalcl  31758  mddmd  32098  mdslmd2i  32127  elat2  32137  xdivpnfrp  32638  isorng  32954  unitdivcld  33438  indpreima  33580  ioosconn  34793  poimirlem26  37054  areacirclem1  37116  isat3  38716  ishlat3N  38763  cvrval5  38825  llnexchb2  39279  lhpoc2N  39425  lhprelat3N  39450  lautcnvle  39499  lautcvr  39502  ltrncnvatb  39548  cdlemb3  40016  cdlemg17h  40078  dih0vbN  40692  djhcvat42  40825  dvh4dimat  40848  mapdordlem2  41047  aks6d1c5lem1  41539  f1o2d2  41644  fsuppind  41745  reltsub1  41863  reltsubadd2  41864  sn-ltmul2d  41938  diophun  42115  jm2.19lem4  42335  ordeldifsucon  42611  orddif0suc  42620  uneqsn  43378  xrralrecnnge  44695  limsupre2lem  45035  prprelb  46779  flsqrt5  46857  lincfsuppcl  47404