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  383  ifptru  1075  sbequ12a  2247  elrnmpt1  5956  fndmdif  7041  weniso  7348  sbcopeq1a  8032  xpord2pred  8128  snmapen  9035  dmttrcl  9713  cfss  10257  posdif  11704  lesub1  11705  lesub0  11728  possumd  11836  ltdivmul  12086  ledivmul  12087  zlem1lt  12611  zltlem1  12612  negelrp  13004  ioon0  13347  fzn  13514  fzrev2  13562  fz1sbc  13574  elfzp1b  13575  sumsqeq0  14140  fz1isolem  14419  sqrtle  15204  absgt0  15268  isershft  15607  incexc2  15781  dvdssubr  16245  gcdn0gt0  16456  divgcdcoprmex  16600  prmdvdssqOLD  16653  pcfac  16829  ramval  16938  iunocv  21226  ltbwe  21591  lmbrf  22756  perfcls  22861  ovolscalem1  25022  itg2mulclem  25256  sineq0  26025  efif1olem4  26046  logge0b  26131  loggt0b  26132  logle1b  26133  loglt1b  26134  atanord  26422  rlimcnp2  26461  bposlem7  26783  lgsprme0  26832  rpvmasum2  27005  sltsubsub2bd  27541  posdifsd  27551  sltmuldivwd  27638  trgcgrg  27756  legov3  27839  opphllem6  27993  ebtwntg  28230  wwlksm1edg  29125  clwlkclwwlk2  29246  hial2eq2  30348  adjsym  31074  cnvadj  31133  eigvalcl  31202  mddmd  31542  mdslmd2i  31571  elat2  31581  xdivpnfrp  32087  isorng  32406  unitdivcld  32870  indpreima  33012  ioosconn  34227  poimirlem26  36503  areacirclem1  36565  isat3  38166  ishlat3N  38213  cvrval5  38275  llnexchb2  38729  lhpoc2N  38875  lhprelat3N  38900  lautcnvle  38949  lautcvr  38952  ltrncnvatb  38998  cdlemb3  39466  cdlemg17h  39528  dih0vbN  40142  djhcvat42  40275  dvh4dimat  40298  mapdordlem2  40497  f1o2d2  41053  fsuppind  41160  reltsub1  41256  reltsubadd2  41257  sn-ltmul2d  41331  diophun  41497  jm2.19lem4  41717  ordeldifsucon  41995  orddif0suc  42004  uneqsn  42762  xrralrecnnge  44087  limsupre2lem  44427  prprelb  46171  flsqrt5  46249  isrnghm  46676  lincfsuppcl  47048