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  1074  sbequ12a  2255  elrnmpt1  5906  fndmdif  6980  weniso  7295  sbcopeq1a  7991  xpord2pred  8085  snmapen  8970  dmttrcl  9636  cfss  10178  posdif  11631  lesub1  11632  lesub0  11655  possumd  11763  ltdivmul  12018  ledivmul  12019  zlem1lt  12545  zltlem1  12546  negelrp  12946  ioon0  13292  fzn  13461  fzrev2  13509  fz1sbc  13521  elfzp1b  13522  sumsqeq0  14104  fz1isolem  14386  sqrtle  15185  absgt0  15250  isershft  15589  incexc2  15763  dvdssubr  16234  gcdn0gt0  16447  divgcdcoprmex  16595  pcfac  16829  ramval  16938  isrnghm  20344  isorng  20764  iunocv  21606  ltbwe  21967  lmbrf  23163  perfcls  23268  ovolscalem1  25430  itg2mulclem  25663  sineq0  26449  efif1olem4  26470  logge0b  26556  loggt0b  26557  logle1b  26558  loglt1b  26559  atanord  26853  rlimcnp2  26892  bposlem7  27217  lgsprme0  27266  rpvmasum2  27439  sltsubsub2bd  28011  posdifsd  28024  sltmuldivwd  28127  pw2gt0divsd  28355  pw2ge0divsd  28356  trgcgrg  28478  legov3  28561  opphllem6  28715  ebtwntg  28945  wwlksm1edg  29844  clwlkclwwlk2  29965  hial2eq2  31069  adjsym  31795  cnvadj  31854  eigvalcl  31923  mddmd  32263  mdslmd2i  32292  elat2  32302  indpreima  32821  xdivpnfrp  32886  ply1dg1rt  33524  unitdivcld  33867  ioosconn  35219  poimirlem26  37625  areacirclem1  37687  isat3  39285  ishlat3N  39332  cvrval5  39394  llnexchb2  39848  lhpoc2N  39994  lhprelat3N  40019  lautcnvle  40068  lautcvr  40071  ltrncnvatb  40117  cdlemb3  40585  cdlemg17h  40647  dih0vbN  41261  djhcvat42  41394  dvh4dimat  41417  mapdordlem2  41616  aks6d1c5lem1  42109  f1o2d2  42206  eluzp1  42280  reltsub1  42359  reltsubadd2  42360  sn-ltmul2d  42446  fsuppind  42563  diophun  42746  jm2.19lem4  42965  ordeldifsucon  43232  orddif0suc  43241  uneqsn  43998  xrralrecnnge  45370  limsupre2lem  45706  modmkpkne  47346  prprelb  47501  flsqrt5  47579  lincfsuppcl  48386