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  2261  elrnmpt1  5904  fndmdif  6983  weniso  7298  sbcopeq1a  7991  xpord2pred  8084  snmapen  8974  dmttrcl  9631  cfss  10176  posdif  11632  lesub1  11633  lesub0  11656  possumd  11764  ltdivmul  12020  ledivmul  12021  zlem1lt  12568  zltlem1  12569  negelrp  12966  ioon0  13313  fzn  13483  fzrev2  13531  fz1sbc  13543  elfzp1b  13544  sumsqeq0  14130  fz1isolem  14412  sqrtle  15211  absgt0  15276  isershft  15615  incexc2  15792  dvdssubr  16263  gcdn0gt0  16476  divgcdcoprmex  16624  pcfac  16859  ramval  16968  isrnghm  20410  isorng  20827  iunocv  21650  ltbwe  22011  lmbrf  23213  perfcls  23318  ovolscalem1  25468  itg2mulclem  25701  sineq0  26476  efif1olem4  26497  logge0b  26583  loggt0b  26584  logle1b  26585  loglt1b  26586  atanord  26879  rlimcnp2  26918  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  29937  clwlkclwwlk2  30061  hial2eq2  31166  adjsym  31892  cnvadj  31951  eigvalcl  32020  mddmd  32360  mdslmd2i  32389  elat2  32399  indpreima  32913  xdivpnfrp  32980  ply1dg1rt  33628  esplyfval1  33705  unitdivcld  34033  ioosconn  35417  poimirlem26  37955  areacirclem1  38017  isat3  39741  ishlat3N  39788  cvrval5  39849  llnexchb2  40303  lhpoc2N  40449  lhprelat3N  40474  lautcnvle  40523  lautcvr  40526  ltrncnvatb  40572  cdlemb3  41040  cdlemg17h  41102  dih0vbN  41716  djhcvat42  41849  dvh4dimat  41872  mapdordlem2  42071  aks6d1c5lem1  42563  f1o2d2  42662  eluzp1  42727  reltsub1  42806  reltsubadd2  42807  sn-ltmul2d  42906  fsuppind  43011  diophun  43193  jm2.19lem4  43408  ordeldifsucon  43675  orddif0suc  43684  uneqsn  44440  xrralrecnnge  45807  limsupre2lem  46140  modmkpkne  47803  prprelb  47964  flsqrt5  48045  lincfsuppcl  48877