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  1087  sbequ12a  2290  elrnmpt1  5937  fndmdif  7023  weniso  7338  sbcopeq1a  8030  mpof1o2d  8105  xpord2pred  8125  snmapen  9019  dmttrcl  9674  cfss  10233  posdif  11691  lesub1  11692  lesub0  11715  possumd  11823  ltdivmul  12077  ledivmul  12078  zlem1lt  12633  zltlem1  12634  negelrp  13038  ioon0  13385  fzn  13555  fzrev2  13603  fz1sbc  13615  elfzp1b  13616  sumsqeq0  14202  fz1isolem  14484  sqrtle  15297  absgt0  15362  isershft  15701  incexc2  15878  dvdssubr  16349  gcdn0gt0  16562  divgcdcoprmex  16710  pcfac  16945  ramval  17054  isrnghm  20500  isorng  20917  iunocv  21740  ltbwe  22104  lmbrf  23327  perfcls  23432  ovolscalem1  25582  itg2mulclem  25815  sineq0  26596  efif1olem4  26617  logge0b  26703  loggt0b  26704  logle1b  26705  loglt1b  26706  atanord  26999  rlimcnp2  27038  bposlem7  27361  lgsprme0  27410  rpvmasum2  27583  ltsubsubs2bd  28184  posdifsd  28198  ltmuldivswd  28301  onsbnd2  28382  pw2gt0divsd  28545  pw2ge0divsd  28546  pw2ltsdiv1d  28552  z12bdaylem1  28570  elreno2  28595  trgcgrg  28691  legov3  28774  opphllem6  28932  plngcplem  28999  ebtwntg  29190  wwlksm1edg  30088  clwlkclwwlk2  30212  hial2eq2  31317  adjsym  32043  cnvadj  32102  eigvalcl  32171  mddmd  32511  mdslmd2i  32540  elat2  32550  indpreima  33049  xdivpnfrp  33116  ply1dg1rt  33779  esplyfval1  33872  unitdivcld  34200  ioosconn  35602  poimirlem26  38150  areacirclem1  38212  isat3  39936  ishlat3N  39983  cvrval5  40044  llnexchb2  40498  lhpoc2N  40644  lhprelat3N  40669  lautcnvle  40718  lautcvr  40721  ltrncnvatb  40767  cdlemb3  41235  cdlemg17h  41297  dih0vbN  41911  djhcvat42  42044  dvh4dimat  42067  mapdordlem2  42266  aks6d1c5lem1  42758  eluzp1  42921  reltsub1  43000  reltsubadd2  43001  sn-ltmul2d  43100  fsuppind  43177  diophun  43359  jm2.19lem4  43574  ordeldifsucon  43841  orddif0suc  43850  uneqsn  44606  xrralrecnnge  45956  limsupre2lem  46289  modmkpkne  47952  prprelb  48113  flsqrt5  48194  lincfsuppcl  49026