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  2254  elrnmpt1  5971  fndmdif  7062  weniso  7374  sbcopeq1a  8074  xpord2pred  8170  snmapen  9078  dmttrcl  9761  cfss  10305  posdif  11756  lesub1  11757  lesub0  11780  possumd  11888  ltdivmul  12143  ledivmul  12144  zlem1lt  12669  zltlem1  12670  negelrp  13068  ioon0  13413  fzn  13580  fzrev2  13628  fz1sbc  13640  elfzp1b  13641  sumsqeq0  14218  fz1isolem  14500  sqrtle  15299  absgt0  15363  isershft  15700  incexc2  15874  dvdssubr  16342  gcdn0gt0  16555  divgcdcoprmex  16703  pcfac  16937  ramval  17046  isrnghm  20441  iunocv  21699  ltbwe  22062  lmbrf  23268  perfcls  23373  ovolscalem1  25548  itg2mulclem  25781  sineq0  26566  efif1olem4  26587  logge0b  26673  loggt0b  26674  logle1b  26675  loglt1b  26676  atanord  26970  rlimcnp2  27009  bposlem7  27334  lgsprme0  27383  rpvmasum2  27556  sltsubsub2bd  28114  posdifsd  28127  sltmuldivwd  28226  trgcgrg  28523  legov3  28606  opphllem6  28760  ebtwntg  28997  wwlksm1edg  29901  clwlkclwwlk2  30022  hial2eq2  31126  adjsym  31852  cnvadj  31911  eigvalcl  31980  mddmd  32320  mdslmd2i  32349  elat2  32359  indpreima  32850  xdivpnfrp  32915  isorng  33329  ply1dg1rt  33604  unitdivcld  33900  ioosconn  35252  poimirlem26  37653  areacirclem1  37715  isat3  39308  ishlat3N  39355  cvrval5  39417  llnexchb2  39871  lhpoc2N  40017  lhprelat3N  40042  lautcnvle  40091  lautcvr  40094  ltrncnvatb  40140  cdlemb3  40608  cdlemg17h  40670  dih0vbN  41284  djhcvat42  41417  dvh4dimat  41440  mapdordlem2  41639  aks6d1c5lem1  42137  f1o2d2  42274  eluzp1  42341  reltsub1  42416  reltsubadd2  42417  sn-ltmul2d  42491  fsuppind  42600  diophun  42784  jm2.19lem4  43004  ordeldifsucon  43272  orddif0suc  43281  uneqsn  44038  xrralrecnnge  45401  limsupre2lem  45739  prprelb  47503  flsqrt5  47581  lincfsuppcl  48330