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 ⊢ (𝜑 → (𝜃 ↔ 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  3bitrrd  309  3bitr2rd  311  pm5.18  384  ifptru  1090  sbequ12a  2289  elrnmpt1  5949  fndmdif  7037  weniso  7354  sbcopeq1a  8044  mpof1o2d  8119  xpord2pred  8139  snmapen  9033  dmttrcl  9688  cfss  10255  posdif  11713  lesub1  11714  lesub0  11737  possumd  11845  ltdivmul  12096  ledivmul  12097  zlem1lt  12652  zltlem1  12653  negelrp  13057  ioon0  13404  fzn  13574  fzrev2  13623  fz1sbc  13635  elfzp1b  13636  sumsqeq0  14222  fz1isolem  14505  sqrtle  15318  absgt0  15383  isershft  15722  incexc2  15899  dvdssubr  16369  gcdn0gt0  16582  divgcdcoprmex  16730  pcfac  16965  ramval  17074  isrnghm  20530  isorng  20975  iunocv  21842  ltbwe  22206  lmbrf  23428  perfcls  23533  ovolscalem1  25683  itg2mulclem  25916  sineq0  26700  efif1olem4  26721  logge0b  26807  loggt0b  26808  logle1b  26809  loglt1b  26810  atanord  27103  rlimcnp2  27142  bposlem7  27465  lgsprme0  27514  rpvmasum2  27687  ltsubsubs2bd  28288  posdifsd  28302  ltmuldivswd  28405  onsbnd2  28486  pw2gt0divsd  28649  pw2ge0divsd  28650  pw2ltsdiv1d  28656  z12bdaylem1  28674  elreno2  28699  trgcgrg  28795  legov3  28878  opphllem6  29044  plngcplem  29078  ebtwntg  29343  wwlksm1edg  30241  clwlkclwwlk2  30365  hial2eq2  31470  adjsym  32196  cnvadj  32255  eigvalcl  32324  mddmd  32664  mdslmd2i  32693  elat2  32703  indpreima  33196  xdivpnfrp  33263  ply1dg1rt  33879  esplyfval1  33972  unitdivcld  34300  ioosconn  35747  nmulle  36717  poimirlem26  38325  areacirclem1  38387  isat3  40109  ishlat3N  40156  cvrval5  40217  llnexchb2  40671  lhpoc2N  40817  lhprelat3N  40842  lautcnvle  40891  lautcvr  40894  ltrncnvatb  40940  cdlemb3  41408  cdlemg17h  41470  dih0vbN  42084  djhcvat42  42217  dvh4dimat  42240  mapdordlem2  42439  aks6d1c5lem1  42931  eluzp1  43096  reltsub1  43175  reltsubadd2  43176  sn-ltmul2d  43275  fsuppind  43350  diophun  43532  jm2.19lem4  43747  ordeldifsucon  44014  orddif0suc  44023  uneqsn  44779  xrralrecnnge  46133  limsupre2lem  46466  modmkpkne  48132  prprelb  48293  flsqrt5  48374  lincfsuppcl  49221