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 223	1 ⊢ (𝜑 → (𝜃 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  3bitrrd  306  3bitr2rd  308  pm5.18  381  ifptru  1075  sbequ12a  2262  elrnmpt1  5916  fndmdif  6995  weniso  7309  sbcopeq1a  8002  xpord2pred  8095  snmapen  8985  dmttrcl  9642  cfss  10187  posdif  11643  lesub1  11644  lesub0  11667  possumd  11775  ltdivmul  12031  ledivmul  12032  zlem1lt  12579  zltlem1  12580  negelrp  12977  ioon0  13324  fzn  13494  fzrev2  13542  fz1sbc  13554  elfzp1b  13555  sumsqeq0  14141  fz1isolem  14423  sqrtle  15222  absgt0  15287  isershft  15626  incexc2  15803  dvdssubr  16274  gcdn0gt0  16487  divgcdcoprmex  16635  pcfac  16870  ramval  16979  isrnghm  20421  isorng  20838  iunocv  21661  ltbwe  22022  lmbrf  23225  perfcls  23330  ovolscalem1  25480  itg2mulclem  25713  sineq0  26488  efif1olem4  26509  logge0b  26595  loggt0b  26596  logle1b  26597  loglt1b  26598  atanord  26891  rlimcnp2  26930  bposlem7  27253  lgsprme0  27302  rpvmasum2  27475  ltsubsubs2bd  28076  posdifsd  28090  ltmuldivswd  28193  onsbnd2  28274  pw2gt0divsd  28437  pw2ge0divsd  28438  pw2ltsdiv1d  28444  z12bdaylem1  28462  elreno2  28487  trgcgrg  28583  legov3  28666  opphllem6  28820  ebtwntg  29051  wwlksm1edg  29949  clwlkclwwlk2  30073  hial2eq2  31178  adjsym  31904  cnvadj  31963  eigvalcl  32032  mddmd  32372  mdslmd2i  32401  elat2  32411  indpreima  32925  xdivpnfrp  32992  ply1dg1rt  33640  esplyfval1  33717  unitdivcld  34045  ioosconn  35429  poimirlem26  37967  areacirclem1  38029  isat3  39753  ishlat3N  39800  cvrval5  39861  llnexchb2  40315  lhpoc2N  40461  lhprelat3N  40486  lautcnvle  40535  lautcvr  40538  ltrncnvatb  40584  cdlemb3  41052  cdlemg17h  41114  dih0vbN  41728  djhcvat42  41861  dvh4dimat  41884  mapdordlem2  42083  aks6d1c5lem1  42575  f1o2d2  42674  eluzp1  42739  reltsub1  42818  reltsubadd2  42819  sn-ltmul2d  42918  fsuppind  43023  diophun  43205  jm2.19lem4  43420  ordeldifsucon  43687  orddif0suc  43696  uneqsn  44452  xrralrecnnge  45819  limsupre2lem  46152  modmkpkne  47809  prprelb  47970  flsqrt5  48051  lincfsuppcl  48883