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  1091  sbequ12a  2289  elrnmpt1  5938  fndmdif  7029  weniso  7352  sbcopeq1a  8043  mpof1o2d  8120  xpord2pred  8140  snmapen  9044  dmttrcl  9700  cfss  10314  posdif  11778  lesub1  11779  lesub0  11802  possumd  11910  ltdivmul  12161  ledivmul  12162  zlem1lt  12717  zltlem1  12718  negelrp  13124  ioon0  13471  fzn  13641  fzrev2  13690  fz1sbc  13702  elfzp1b  13703  sumsqeq0  14290  fz1isolem  14573  sqrtle  15394  absgt0  15459  isershft  15798  incexc2  15974  dvdssubr  16442  gcdn0gt0  16655  divgcdcoprmex  16803  pcfac  17038  ramval  17147  isrnghm  20632  isorng  21079  iunocv  21948  ltbwe  22314  lmbrf  23539  perfcls  23644  ovolscalem1  25795  itg2mulclem  26028  sineq0  26815  efif1olem4  26836  logge0b  26922  loggt0b  26923  logle1b  26924  loglt1b  26925  atanord  27218  rlimcnp2  27257  bposlem7  27580  lgsprme0  27629  rpvmasum2  27802  ltsubsubs2bd  28403  posdifsd  28417  ltmuldivswd  28520  onsbnd2  28601  pw2gt0divsd  28764  pw2ge0divsd  28765  pw2ltsdiv1d  28771  z12bdaylem1  28789  elreno2  28814  trgcgrg  28911  legov3  28994  opphllem6  29161  plngcplem  29196  ebtwntg  29493  wwlksm1edg  30403  clwlkclwwlk2  30527  hial2eq2  31642  adjsym  32368  cnvadj  32427  eigvalcl  32496  mddmd  32836  mdslmd2i  32865  elat2  32875  indpreima  33365  xdivpnfrp  33432  ply1dg1rt  34045  esplyfval1  34138  unitdivcld  34466  ioosconn  35933  nmulle  36888  poimirlem26  38484  areacirclem1  38546  isat3  40284  ishlat3N  40331  cvrval5  40392  llnexchb2  40846  lhpoc2N  40992  lhprelat3N  41017  lautcnvle  41066  lautcvr  41069  ltrncnvatb  41115  cdlemb3  41583  cdlemg17h  41645  dih0vbN  42259  djhcvat42  42392  dvh4dimat  42415  mapdordlem2  42614  aks6d1c5lem1  43106  eluzp1  43286  reltsub1  43365  reltsubadd2  43366  sn-ltmul2d  43465  fsuppind  43540  diophun  43722  jm2.19lem4  43937  ordeldifsucon  44204  orddif0suc  44213  uneqsn  44969  xrralrecnnge  46323  limsupre2lem  46656  tmachlem-agreeprod  47869  modmkpkne  48359  prprelb  48520  flsqrt5  48601  lincfsuppcl  49447