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  386  ifptru  1071  sbequ12a  2253  elrnmpt1  5794  fndmdif  6789  weniso  7086  sbcopeq1a  7730  snmapen  8573  cfss  9676  posdif  11122  lesub1  11123  lesub0  11146  possumd  11254  ltdivmul  11504  ledivmul  11505  zlem1lt  12022  zltlem1  12023  negelrp  12410  ioon0  12752  fzn  12918  fzrev2  12966  fz1sbc  12978  elfzp1b  12979  sumsqeq0  13538  fz1isolem  13815  sqrtle  14612  absgt0  14676  isershft  15012  incexc2  15185  dvdssubr  15647  gcdn0gt0  15856  divgcdcoprmex  16000  pcfac  16225  ramval  16334  iunocv  20370  ltbwe  20712  lmbrf  21865  perfcls  21970  ovolscalem1  24117  itg2mulclem  24350  sineq0  25116  efif1olem4  25137  logge0b  25222  loggt0b  25223  logle1b  25224  loglt1b  25225  atanord  25513  rlimcnp2  25552  bposlem7  25874  lgsprme0  25923  rpvmasum2  26096  trgcgrg  26309  legov3  26392  opphllem6  26546  ebtwntg  26776  wwlksm1edg  27667  clwlkclwwlk2  27788  hial2eq2  28890  adjsym  29616  cnvadj  29675  eigvalcl  29744  mddmd  30084  mdslmd2i  30113  elat2  30123  xdivpnfrp  30635  isorng  30923  unitdivcld  31254  indpreima  31394  ioosconn  32607  pdivsq  33094  poimirlem26  35083  areacirclem1  35145  isat3  36603  ishlat3N  36650  cvrval5  36711  llnexchb2  37165  lhpoc2N  37311  lhprelat3N  37336  lautcnvle  37385  lautcvr  37388  ltrncnvatb  37434  cdlemb3  37902  cdlemg17h  37964  dih0vbN  38578  djhcvat42  38711  dvh4dimat  38734  mapdordlem2  38933  fsuppind  39456  reltsub1  39524  reltsubadd2  39525  sn-ltmul2d  39586  diophun  39714  jm2.19lem4  39933  uneqsn  40726  xrralrecnnge  42026  limsupre2lem  42366  prprelb  44033  flsqrt5  44111  isrnghm  44516  lincfsuppcl  44822