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  2291  elrnmpt1  5948  fndmdif  7038  weniso  7360  sbcopeq1a  8049  mpof1o2d  8126  xpord2pred  8146  snmapen  9048  dmttrcl  9703  cfss  10270  posdif  11734  lesub1  11735  lesub0  11758  possumd  11866  ltdivmul  12117  ledivmul  12118  zlem1lt  12673  zltlem1  12674  negelrp  13079  ioon0  13426  fzn  13596  fzrev2  13645  fz1sbc  13657  elfzp1b  13658  sumsqeq0  14245  fz1isolem  14528  sqrtle  15349  absgt0  15414  isershft  15753  incexc2  15929  dvdssubr  16399  gcdn0gt0  16612  divgcdcoprmex  16760  pcfac  16995  ramval  17104  isrnghm  20583  isorng  21028  iunocv  21895  ltbwe  22261  lmbrf  23486  perfcls  23591  ovolscalem1  25742  itg2mulclem  25975  sineq0  26759  efif1olem4  26780  logge0b  26866  loggt0b  26867  logle1b  26868  loglt1b  26869  atanord  27162  rlimcnp2  27201  bposlem7  27524  lgsprme0  27573  rpvmasum2  27746  ltsubsubs2bd  28347  posdifsd  28361  ltmuldivswd  28464  onsbnd2  28545  pw2gt0divsd  28708  pw2ge0divsd  28709  pw2ltsdiv1d  28715  z12bdaylem1  28733  elreno2  28758  trgcgrg  28855  legov3  28938  opphllem6  29105  plngcplem  29140  ebtwntg  29425  wwlksm1edg  30335  clwlkclwwlk2  30459  hial2eq2  31574  adjsym  32300  cnvadj  32359  eigvalcl  32428  mddmd  32768  mdslmd2i  32797  elat2  32807  indpreima  33298  xdivpnfrp  33365  ply1dg1rt  33977  esplyfval1  34070  unitdivcld  34398  ioosconn  35813  nmulle  36784  poimirlem26  38382  areacirclem1  38444  isat3  40167  ishlat3N  40214  cvrval5  40275  llnexchb2  40729  lhpoc2N  40875  lhprelat3N  40900  lautcnvle  40949  lautcvr  40952  ltrncnvatb  40998  cdlemb3  41466  cdlemg17h  41528  dih0vbN  42142  djhcvat42  42275  dvh4dimat  42298  mapdordlem2  42497  aks6d1c5lem1  42989  eluzp1  43169  reltsub1  43248  reltsubadd2  43249  sn-ltmul2d  43348  fsuppind  43423  diophun  43605  jm2.19lem4  43820  ordeldifsucon  44087  orddif0suc  44096  uneqsn  44852  xrralrecnnge  46206  limsupre2lem  46539  tmachlem-agreeprod  47752  modmkpkne  48242  prprelb  48403  flsqrt5  48484  lincfsuppcl  49330