Theorem bitr2d 279

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  3bitrrd  305  3bitr2rd  307  pm5.18  380  ifptru  1072  sbequ12a  2244  elrnmpt1  5956  fndmdif  7042  weniso  7353  sbcopeq1a  8037  xpord2pred  8133  snmapen  9040  dmttrcl  9718  cfss  10262  posdif  11711  lesub1  11712  lesub0  11735  possumd  11843  ltdivmul  12093  ledivmul  12094  zlem1lt  12618  zltlem1  12619  negelrp  13011  ioon0  13354  fzn  13521  fzrev2  13569  fz1sbc  13581  elfzp1b  13582  sumsqeq0  14147  fz1isolem  14426  sqrtle  15211  absgt0  15275  isershft  15614  incexc2  15788  dvdssubr  16252  gcdn0gt0  16463  divgcdcoprmex  16607  prmdvdssqOLD  16660  pcfac  16836  ramval  16945  isrnghm  20332  iunocv  21453  ltbwe  21818  lmbrf  22984  perfcls  23089  ovolscalem1  25262  itg2mulclem  25496  sineq0  26269  efif1olem4  26290  logge0b  26375  loggt0b  26376  logle1b  26377  loglt1b  26378  atanord  26668  rlimcnp2  26707  bposlem7  27029  lgsprme0  27078  rpvmasum2  27251  sltsubsub2bd  27790  posdifsd  27800  sltmuldivwd  27887  trgcgrg  28033  legov3  28116  opphllem6  28270  ebtwntg  28507  wwlksm1edg  29402  clwlkclwwlk2  29523  hial2eq2  30627  adjsym  31353  cnvadj  31412  eigvalcl  31481  mddmd  31821  mdslmd2i  31850  elat2  31860  xdivpnfrp  32366  isorng  32687  unitdivcld  33179  indpreima  33321  ioosconn  34536  poimirlem26  36817  areacirclem1  36879  isat3  38480  ishlat3N  38527  cvrval5  38589  llnexchb2  39043  lhpoc2N  39189  lhprelat3N  39214  lautcnvle  39263  lautcvr  39266  ltrncnvatb  39312  cdlemb3  39780  cdlemg17h  39842  dih0vbN  40456  djhcvat42  40589  dvh4dimat  40612  mapdordlem2  40811  f1o2d2  41361  fsuppind  41464  reltsub1  41561  reltsubadd2  41562  sn-ltmul2d  41636  diophun  41813  jm2.19lem4  42033  ordeldifsucon  42311  orddif0suc  42320  uneqsn  43078  xrralrecnnge  44398  limsupre2lem  44738  prprelb  46482  flsqrt5  46560  lincfsuppcl  47181