Theorem bitr2d 282

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  3bitrrd  308  3bitr2rd  310  pm5.18  383  ifptru  1083  sbequ12a  2279  elrnmpt1  5925  fndmdif  7008  weniso  7323  sbcopeq1a  8015  mpof1o2d  8089  xpord2pred  8109  snmapen  9004  dmttrcl  9662  cfss  10208  posdif  11666  lesub1  11667  lesub0  11690  possumd  11798  ltdivmul  12053  ledivmul  12054  zlem1lt  12609  zltlem1  12610  negelrp  13014  ioon0  13361  fzn  13531  fzrev2  13579  fz1sbc  13591  elfzp1b  13592  sumsqeq0  14178  fz1isolem  14460  sqrtle  15259  absgt0  15324  isershft  15663  incexc2  15840  dvdssubr  16311  gcdn0gt0  16524  divgcdcoprmex  16672  pcfac  16907  ramval  17016  isrnghm  20458  isorng  20879  iunocv  21702  ltbwe  22066  lmbrf  23289  perfcls  23394  ovolscalem1  25544  itg2mulclem  25777  sineq0  26555  efif1olem4  26576  logge0b  26662  loggt0b  26663  logle1b  26664  loglt1b  26665  atanord  26958  rlimcnp2  26997  bposlem7  27320  lgsprme0  27369  rpvmasum2  27542  ltsubsubs2bd  28143  posdifsd  28157  ltmuldivswd  28260  onsbnd2  28341  pw2gt0divsd  28504  pw2ge0divsd  28505  pw2ltsdiv1d  28511  z12bdaylem1  28529  elreno2  28554  trgcgrg  28650  legov3  28733  opphllem6  28887  ebtwntg  29118  wwlksm1edg  30016  clwlkclwwlk2  30140  hial2eq2  31245  adjsym  31971  cnvadj  32030  eigvalcl  32099  mddmd  32439  mdslmd2i  32468  elat2  32478  indpreima  32993  xdivpnfrp  33060  ply1dg1rt  33720  esplyfval1  33814  unitdivcld  34142  ioosconn  35535  poimirlem26  38083  areacirclem1  38145  isat3  39869  ishlat3N  39916  cvrval5  39977  llnexchb2  40431  lhpoc2N  40577  lhprelat3N  40602  lautcnvle  40651  lautcvr  40654  ltrncnvatb  40700  cdlemb3  41168  cdlemg17h  41230  dih0vbN  41844  djhcvat42  41977  dvh4dimat  42000  mapdordlem2  42199  aks6d1c5lem1  42691  eluzp1  42854  reltsub1  42933  reltsubadd2  42934  sn-ltmul2d  43033  fsuppind  43110  diophun  43292  jm2.19lem4  43507  ordeldifsucon  43774  orddif0suc  43783  uneqsn  44539  xrralrecnnge  45903  limsupre2lem  46236  modmkpkne  47899  prprelb  48060  flsqrt5  48141  lincfsuppcl  48973