Theorem bitr2d 282

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  3bitrrd  308  3bitr2rd  310  pm5.18  385  ifptru  1068  sbequ12a  2256  elrnmpt1  5830  fndmdif  6812  weniso  7107  sbcopeq1a  7748  snmapen  8590  cfss  9687  posdif  11133  lesub1  11134  lesub0  11157  possumd  11265  ltdivmul  11515  ledivmul  11516  zlem1lt  12035  zltlem1  12036  negelrp  12423  ioon0  12765  fzn  12924  fzrev2  12972  fz1sbc  12984  elfzp1b  12985  sumsqeq0  13543  fz1isolem  13820  sqrtle  14620  absgt0  14684  isershft  15020  incexc2  15193  dvdssubr  15655  gcdn0gt0  15866  divgcdcoprmex  16010  pcfac  16235  ramval  16344  ltbwe  20253  mhpinvcl  20339  iunocv  20825  lmbrf  21868  perfcls  21973  ovolscalem1  24114  itg2mulclem  24347  sineq0  25109  efif1olem4  25129  logge0b  25214  loggt0b  25215  logle1b  25216  loglt1b  25217  atanord  25505  rlimcnp2  25544  bposlem7  25866  lgsprme0  25915  rpvmasum2  26088  trgcgrg  26301  legov3  26384  opphllem6  26538  ebtwntg  26768  wwlksm1edg  27659  clwlkclwwlk2  27781  hial2eq2  28884  adjsym  29610  cnvadj  29669  eigvalcl  29738  mddmd  30078  mdslmd2i  30107  elat2  30117  xdivpnfrp  30609  isorng  30872  unitdivcld  31144  indpreima  31284  ioosconn  32494  pdivsq  32981  poimirlem26  34933  areacirclem1  34997  isat3  36458  ishlat3N  36505  cvrval5  36566  llnexchb2  37020  lhpoc2N  37166  lhprelat3N  37191  lautcnvle  37240  lautcvr  37243  ltrncnvatb  37289  cdlemb3  37757  cdlemg17h  37819  dih0vbN  38433  djhcvat42  38566  dvh4dimat  38589  mapdordlem2  38788  reltsub1  39236  reltsubadd2  39237  diophun  39390  jm2.19lem4  39609  uneqsn  40393  xrralrecnnge  41682  limsupre2lem  42025  prprelb  43698  flsqrt5  43777  isrnghm  44183  lincfsuppcl  44488