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  1075  sbequ12a  2262  elrnmpt1  5907  fndmdif  6986  weniso  7300  sbcopeq1a  7993  xpord2pred  8086  snmapen  8976  dmttrcl  9631  cfss  10176  posdif  11631  lesub1  11632  lesub0  11655  possumd  11763  ltdivmul  12018  ledivmul  12019  zlem1lt  12544  zltlem1  12545  negelrp  12941  ioon0  13288  fzn  13457  fzrev2  13505  fz1sbc  13517  elfzp1b  13518  sumsqeq0  14103  fz1isolem  14385  sqrtle  15184  absgt0  15249  isershft  15588  incexc2  15762  dvdssubr  16233  gcdn0gt0  16446  divgcdcoprmex  16594  pcfac  16828  ramval  16937  isrnghm  20379  isorng  20796  iunocv  21638  ltbwe  22000  lmbrf  23203  perfcls  23308  ovolscalem1  25458  itg2mulclem  25691  sineq0  26473  efif1olem4  26494  logge0b  26580  loggt0b  26581  logle1b  26582  loglt1b  26583  atanord  26877  rlimcnp2  26916  bposlem7  27241  lgsprme0  27290  rpvmasum2  27463  ltsubsubs2bd  28064  posdifsd  28078  ltmuldivswd  28181  onsbnd2  28262  pw2gt0divsd  28425  pw2ge0divsd  28426  pw2ltsdiv1d  28432  z12bdaylem1  28450  elreno2  28475  trgcgrg  28571  legov3  28654  opphllem6  28808  ebtwntg  29039  wwlksm1edg  29938  clwlkclwwlk2  30062  hial2eq2  31167  adjsym  31893  cnvadj  31952  eigvalcl  32021  mddmd  32361  mdslmd2i  32390  elat2  32400  indpreima  32930  xdivpnfrp  32997  ply1dg1rt  33645  esplyfval1  33722  unitdivcld  34051  ioosconn  35435  poimirlem26  37958  areacirclem1  38020  isat3  39744  ishlat3N  39791  cvrval5  39852  llnexchb2  40306  lhpoc2N  40452  lhprelat3N  40477  lautcnvle  40526  lautcvr  40529  ltrncnvatb  40575  cdlemb3  41043  cdlemg17h  41105  dih0vbN  41719  djhcvat42  41852  dvh4dimat  41875  mapdordlem2  42074  aks6d1c5lem1  42567  f1o2d2  42666  eluzp1  42738  reltsub1  42817  reltsubadd2  42818  sn-ltmul2d  42917  fsuppind  43022  diophun  43204  jm2.19lem4  43423  ordeldifsucon  43690  orddif0suc  43699  uneqsn  44455  xrralrecnnge  45822  limsupre2lem  46156  modmkpkne  47795  prprelb  47950  flsqrt5  48028  lincfsuppcl  48847