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  310  3bitr2rd  312  pm5.18  387  ifptru  1072  sbequ12a  2254  elrnmpt1  5800  fndmdif  6804  weniso  7102  sbcopeq1a  7753  snmapen  8610  cfss  9718  posdif  11164  lesub1  11165  lesub0  11188  possumd  11296  ltdivmul  11546  ledivmul  11547  zlem1lt  12066  zltlem1  12067  negelrp  12456  ioon0  12798  fzn  12965  fzrev2  13013  fz1sbc  13025  elfzp1b  13026  sumsqeq0  13585  fz1isolem  13864  sqrtle  14661  absgt0  14725  isershft  15061  incexc2  15234  dvdssubr  15699  gcdn0gt0  15910  divgcdcoprmex  16055  prmdvdssqOLD  16108  pcfac  16283  ramval  16392  iunocv  20439  ltbwe  20797  lmbrf  21953  perfcls  22058  ovolscalem1  24206  itg2mulclem  24439  sineq0  25208  efif1olem4  25229  logge0b  25314  loggt0b  25315  logle1b  25316  loglt1b  25317  atanord  25605  rlimcnp2  25644  bposlem7  25966  lgsprme0  26015  rpvmasum2  26188  trgcgrg  26401  legov3  26484  opphllem6  26638  ebtwntg  26868  wwlksm1edg  27759  clwlkclwwlk2  27880  hial2eq2  28982  adjsym  29708  cnvadj  29767  eigvalcl  29836  mddmd  30176  mdslmd2i  30205  elat2  30215  xdivpnfrp  30724  isorng  31017  unitdivcld  31365  indpreima  31505  ioosconn  32718  xpord2pred  33340  xpord3pred  33346  poimirlem26  35356  areacirclem1  35418  isat3  36876  ishlat3N  36923  cvrval5  36984  llnexchb2  37438  lhpoc2N  37584  lhprelat3N  37609  lautcnvle  37658  lautcvr  37661  ltrncnvatb  37707  cdlemb3  38175  cdlemg17h  38237  dih0vbN  38851  djhcvat42  38984  dvh4dimat  39007  mapdordlem2  39206  fsuppind  39777  reltsub1  39859  reltsubadd2  39860  sn-ltmul2d  39921  diophun  40080  jm2.19lem4  40299  uneqsn  41092  xrralrecnnge  42386  limsupre2lem  42725  prprelb  44394  flsqrt5  44472  isrnghm  44876  lincfsuppcl  45180