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  380  ifptru  1072  sbequ12a  2241  elrnmpt1  5959  fndmdif  7048  weniso  7359  sbcopeq1a  8052  xpord2pred  8148  snmapen  9061  dmttrcl  9744  cfss  10288  posdif  11737  lesub1  11738  lesub0  11761  possumd  11869  ltdivmul  12119  ledivmul  12120  zlem1lt  12644  zltlem1  12645  negelrp  13039  ioon0  13382  fzn  13549  fzrev2  13597  fz1sbc  13609  elfzp1b  13610  sumsqeq0  14175  fz1isolem  14455  sqrtle  15240  absgt0  15304  isershft  15643  incexc2  15817  dvdssubr  16282  gcdn0gt0  16493  divgcdcoprmex  16637  prmdvdssqOLD  16690  pcfac  16868  ramval  16977  isrnghm  20385  iunocv  21618  ltbwe  21990  lmbrf  23195  perfcls  23300  ovolscalem1  25473  itg2mulclem  25707  sineq0  26489  efif1olem4  26510  logge0b  26596  loggt0b  26597  logle1b  26598  loglt1b  26599  atanord  26890  rlimcnp2  26929  bposlem7  27254  lgsprme0  27303  rpvmasum2  27476  sltsubsub2bd  28025  posdifsd  28038  sltmuldivwd  28135  trgcgrg  28376  legov3  28459  opphllem6  28613  ebtwntg  28850  wwlksm1edg  29749  clwlkclwwlk2  29870  hial2eq2  30974  adjsym  31700  cnvadj  31759  eigvalcl  31828  mddmd  32168  mdslmd2i  32197  elat2  32207  xdivpnfrp  32718  isorng  33085  unitdivcld  33589  indpreima  33731  ioosconn  34944  poimirlem26  37206  areacirclem1  37268  isat3  38865  ishlat3N  38912  cvrval5  38974  llnexchb2  39428  lhpoc2N  39574  lhprelat3N  39599  lautcnvle  39648  lautcvr  39651  ltrncnvatb  39697  cdlemb3  40165  cdlemg17h  40227  dih0vbN  40841  djhcvat42  40974  dvh4dimat  40997  mapdordlem2  41196  aks6d1c5lem1  41693  f1o2d2  41809  fsuppind  41905  reltsub1  42023  reltsubadd2  42024  sn-ltmul2d  42098  diophun  42275  jm2.19lem4  42495  ordeldifsucon  42770  orddif0suc  42779  uneqsn  43537  xrralrecnnge  44852  limsupre2lem  45192  prprelb  46935  flsqrt5  47013  lincfsuppcl  47609