Theorem bitr2d 280

Description: Deduction form of bitr2i 276. (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 279	. 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  306  3bitr2rd  308  pm5.18  383  ifptru  1075  sbequ12a  2247  elrnmpt1  5958  fndmdif  7044  weniso  7351  sbcopeq1a  8035  xpord2pred  8131  snmapen  9038  dmttrcl  9716  cfss  10260  posdif  11707  lesub1  11708  lesub0  11731  possumd  11839  ltdivmul  12089  ledivmul  12090  zlem1lt  12614  zltlem1  12615  negelrp  13007  ioon0  13350  fzn  13517  fzrev2  13565  fz1sbc  13577  elfzp1b  13578  sumsqeq0  14143  fz1isolem  14422  sqrtle  15207  absgt0  15271  isershft  15610  incexc2  15784  dvdssubr  16248  gcdn0gt0  16459  divgcdcoprmex  16603  prmdvdssqOLD  16656  pcfac  16832  ramval  16941  iunocv  21234  ltbwe  21599  lmbrf  22764  perfcls  22869  ovolscalem1  25030  itg2mulclem  25264  sineq0  26033  efif1olem4  26054  logge0b  26139  loggt0b  26140  logle1b  26141  loglt1b  26142  atanord  26432  rlimcnp2  26471  bposlem7  26793  lgsprme0  26842  rpvmasum2  27015  sltsubsub2bd  27551  posdifsd  27561  sltmuldivwd  27648  trgcgrg  27766  legov3  27849  opphllem6  28003  ebtwntg  28240  wwlksm1edg  29135  clwlkclwwlk2  29256  hial2eq2  30360  adjsym  31086  cnvadj  31145  eigvalcl  31214  mddmd  31554  mdslmd2i  31583  elat2  31593  xdivpnfrp  32099  isorng  32417  unitdivcld  32881  indpreima  33023  ioosconn  34238  poimirlem26  36514  areacirclem1  36576  isat3  38177  ishlat3N  38224  cvrval5  38286  llnexchb2  38740  lhpoc2N  38886  lhprelat3N  38911  lautcnvle  38960  lautcvr  38963  ltrncnvatb  39009  cdlemb3  39477  cdlemg17h  39539  dih0vbN  40153  djhcvat42  40286  dvh4dimat  40309  mapdordlem2  40508  f1o2d2  41055  fsuppind  41162  reltsub1  41259  reltsubadd2  41260  sn-ltmul2d  41334  diophun  41511  jm2.19lem4  41731  ordeldifsucon  42009  orddif0suc  42018  uneqsn  42776  xrralrecnnge  44100  limsupre2lem  44440  prprelb  46184  flsqrt5  46262  isrnghm  46690  lincfsuppcl  47094