Theorem bitr2d 269

Description: Deduction form of bitr2i 265. (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 268	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4	3	bicomd 213	1 ⊢ (𝜑 → (𝜃 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 196

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 197

This theorem is referenced by:  3bitrrd  295  3bitr2rd  297  pm5.18  370  ifptru  1043  sbequ12a  2151  elrnmpt1  5406  fndmdif  6361  weniso  6644  sbcopeq1a  7264  cfss  9125  posdif  10559  lesub1  10560  lesub0  10583  possumd  10690  ltdivmul  10936  ledivmul  10937  zlem1lt  11467  zltlem1  11468  negelrp  11902  ioon0  12239  fzn  12395  fzrev2  12442  fz1sbc  12454  elfzp1b  12455  sumsqeq0  12982  fz1isolem  13283  sqrtle  14045  absgt0  14108  isershft  14438  incexc2  14614  dvdssubr  15074  gcdn0gt0  15286  divgcdcoprmex  15427  pcfac  15650  ramval  15759  ltbwe  19520  iunocv  20073  lmbrf  21112  perfcls  21217  ovolscalem1  23327  itg2mulclem  23558  sineq0  24318  efif1olem4  24336  logge0b  24422  loggt0b  24423  logle1b  24424  loglt1b  24425  atanord  24699  rlimcnp2  24738  bposlem7  25060  lgsprme0  25109  rpvmasum2  25246  trgcgrg  25455  legov3  25538  opphllem6  25689  ebtwntg  25907  wwlksm1edg  26835  hial2eq2  28092  adjsym  28820  cnvadj  28879  eigvalcl  28948  mddmd  29288  mdslmd2i  29317  elat2  29327  xdivpnfrp  29769  isorng  29927  unitdivcld  30075  indpreima  30215  ioosconn  31355  pdivsq  31761  poimirlem26  33565  areacirclem1  33630  isat3  34912  ishlat3N  34959  cvrval5  35019  llnexchb2  35473  lhpoc2N  35619  lhprelat3N  35644  lautcnvle  35693  lautcvr  35696  ltrncnvatb  35742  cdlemb3  36211  cdlemg17h  36273  dih0vbN  36888  djhcvat42  37021  dvh4dimat  37044  mapdordlem2  37243  diophun  37654  jm2.19lem4  37876  uneqsn  38638  xrralrecnnge  39926  limsupre2lem  40274  flsqrt5  41834  isrnghm  42217  lincfsuppcl  42527