Theorem bitr2d 283

Description: Deduction form of bitr2i 279. (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 282	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4	3	bicomd 226	1 ⊢ (𝜑 → (𝜃 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  3bitrrd  309  3bitr2rd  311  pm5.18  384  ifptru  1089  sbequ12a  2288  elrnmpt1  5950  fndmdif  7037  weniso  7352  sbcopeq1a  8045  mpof1o2d  8120  xpord2pred  8140  snmapen  9034  dmttrcl  9689  cfss  10248  posdif  11706  lesub1  11707  lesub0  11730  possumd  11838  ltdivmul  12089  ledivmul  12090  zlem1lt  12645  zltlem1  12646  negelrp  13050  ioon0  13397  fzn  13567  fzrev2  13615  fz1sbc  13627  elfzp1b  13628  sumsqeq0  14214  fz1isolem  14497  sqrtle  15310  absgt0  15375  isershft  15714  incexc2  15891  dvdssubr  16362  gcdn0gt0  16575  divgcdcoprmex  16723  pcfac  16958  ramval  17067  isrnghm  20522  isorng  20943  iunocv  21810  ltbwe  22174  lmbrf  23396  perfcls  23501  ovolscalem1  25651  itg2mulclem  25884  sineq0  26665  efif1olem4  26686  logge0b  26772  loggt0b  26773  logle1b  26774  loglt1b  26775  atanord  27068  rlimcnp2  27107  bposlem7  27430  lgsprme0  27479  rpvmasum2  27652  ltsubsubs2bd  28253  posdifsd  28267  ltmuldivswd  28370  onsbnd2  28451  pw2gt0divsd  28614  pw2ge0divsd  28615  pw2ltsdiv1d  28621  z12bdaylem1  28639  elreno2  28664  trgcgrg  28760  legov3  28843  opphllem6  29008  plngcplem  29041  ebtwntg  29298  wwlksm1edg  30196  clwlkclwwlk2  30320  hial2eq2  31425  adjsym  32151  cnvadj  32210  eigvalcl  32279  mddmd  32619  mdslmd2i  32648  elat2  32658  indpreima  33151  xdivpnfrp  33218  ply1dg1rt  33836  esplyfval1  33929  unitdivcld  34257  ioosconn  35693  poimirlem26  38241  areacirclem1  38303  isat3  40027  ishlat3N  40074  cvrval5  40135  llnexchb2  40589  lhpoc2N  40735  lhprelat3N  40760  lautcnvle  40809  lautcvr  40812  ltrncnvatb  40858  cdlemb3  41326  cdlemg17h  41388  dih0vbN  42002  djhcvat42  42135  dvh4dimat  42158  mapdordlem2  42357  aks6d1c5lem1  42849  eluzp1  43014  reltsub1  43093  reltsubadd2  43094  sn-ltmul2d  43193  fsuppind  43270  diophun  43452  jm2.19lem4  43667  ordeldifsucon  43934  orddif0suc  43943  uneqsn  44699  xrralrecnnge  46053  limsupre2lem  46386  modmkpkne  48049  prprelb  48210  flsqrt5  48291  lincfsuppcl  49138