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  1075  sbequ12a  2262  elrnmpt1  5910  fndmdif  6989  weniso  7303  sbcopeq1a  7996  xpord2pred  8090  snmapen  8980  dmttrcl  9635  cfss  10180  posdif  11635  lesub1  11636  lesub0  11659  possumd  11767  ltdivmul  12022  ledivmul  12023  zlem1lt  12548  zltlem1  12549  negelrp  12945  ioon0  13292  fzn  13461  fzrev2  13509  fz1sbc  13521  elfzp1b  13522  sumsqeq0  14107  fz1isolem  14389  sqrtle  15188  absgt0  15253  isershft  15592  incexc2  15766  dvdssubr  16237  gcdn0gt0  16450  divgcdcoprmex  16598  pcfac  16832  ramval  16941  isrnghm  20382  isorng  20799  iunocv  21641  ltbwe  22004  lmbrf  23209  perfcls  23314  ovolscalem1  25475  itg2mulclem  25708  sineq0  26494  efif1olem4  26515  logge0b  26601  loggt0b  26602  logle1b  26603  loglt1b  26604  atanord  26898  rlimcnp2  26937  bposlem7  27262  lgsprme0  27311  rpvmasum2  27484  ltsubsubs2bd  28085  posdifsd  28099  ltmuldivswd  28202  onsbnd2  28283  pw2gt0divsd  28446  pw2ge0divsd  28447  pw2ltsdiv1d  28453  z12bdaylem1  28471  elreno2  28496  trgcgrg  28592  legov3  28675  opphllem6  28829  ebtwntg  29060  wwlksm1edg  29959  clwlkclwwlk2  30083  hial2eq2  31187  adjsym  31913  cnvadj  31972  eigvalcl  32041  mddmd  32381  mdslmd2i  32410  elat2  32420  indpreima  32950  xdivpnfrp  33017  ply1dg1rt  33665  esplyfval1  33742  unitdivcld  34071  ioosconn  35454  poimirlem26  37860  areacirclem1  37922  isat3  39646  ishlat3N  39693  cvrval5  39754  llnexchb2  40208  lhpoc2N  40354  lhprelat3N  40379  lautcnvle  40428  lautcvr  40431  ltrncnvatb  40477  cdlemb3  40945  cdlemg17h  41007  dih0vbN  41621  djhcvat42  41754  dvh4dimat  41777  mapdordlem2  41976  aks6d1c5lem1  42469  f1o2d2  42568  eluzp1  42640  reltsub1  42719  reltsubadd2  42720  sn-ltmul2d  42806  fsuppind  42911  diophun  43093  jm2.19lem4  43312  ordeldifsucon  43579  orddif0suc  43588  uneqsn  44344  xrralrecnnge  45711  limsupre2lem  46045  modmkpkne  47684  prprelb  47839  flsqrt5  47917  lincfsuppcl  48736