Theorem bitr2d 279

Description: Deduction form of bitr2i 275. (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 278	. 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  305  3bitr2rd  307  pm5.18  382  ifptru  1072  sbequ12a  2250  elrnmpt1  5856  fndmdif  6901  weniso  7205  sbcopeq1a  7863  snmapen  8782  cfss  9952  posdif  11398  lesub1  11399  lesub0  11422  possumd  11530  ltdivmul  11780  ledivmul  11781  zlem1lt  12302  zltlem1  12303  negelrp  12692  ioon0  13034  fzn  13201  fzrev2  13249  fz1sbc  13261  elfzp1b  13262  sumsqeq0  13824  fz1isolem  14103  sqrtle  14900  absgt0  14964  isershft  15303  incexc2  15478  dvdssubr  15942  gcdn0gt0  16153  divgcdcoprmex  16299  prmdvdssqOLD  16352  pcfac  16528  ramval  16637  iunocv  20798  ltbwe  21155  lmbrf  22319  perfcls  22424  ovolscalem1  24582  itg2mulclem  24816  sineq0  25585  efif1olem4  25606  logge0b  25691  loggt0b  25692  logle1b  25693  loglt1b  25694  atanord  25982  rlimcnp2  26021  bposlem7  26343  lgsprme0  26392  rpvmasum2  26565  trgcgrg  26780  legov3  26863  opphllem6  27017  ebtwntg  27253  wwlksm1edg  28147  clwlkclwwlk2  28268  hial2eq2  29370  adjsym  30096  cnvadj  30155  eigvalcl  30224  mddmd  30564  mdslmd2i  30593  elat2  30603  xdivpnfrp  31109  isorng  31400  unitdivcld  31753  indpreima  31893  ioosconn  33109  dmttrcl  33707  xpord2pred  33719  xpord3pred  33725  poimirlem26  35730  areacirclem1  35792  isat3  37248  ishlat3N  37295  cvrval5  37356  llnexchb2  37810  lhpoc2N  37956  lhprelat3N  37981  lautcnvle  38030  lautcvr  38033  ltrncnvatb  38079  cdlemb3  38547  cdlemg17h  38609  dih0vbN  39223  djhcvat42  39356  dvh4dimat  39379  mapdordlem2  39578  fsuppind  40202  reltsub1  40290  reltsubadd2  40291  sn-ltmul2d  40352  diophun  40511  jm2.19lem4  40730  uneqsn  41522  xrralrecnnge  42820  limsupre2lem  43155  prprelb  44856  flsqrt5  44934  isrnghm  45338  lincfsuppcl  45642