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  5910  fndmdif  6989  weniso  7302  sbcopeq1a  7995  xpord2pred  8089  snmapen  8979  dmttrcl  9634  cfss  10179  posdif  11634  lesub1  11635  lesub0  11658  possumd  11766  ltdivmul  12021  ledivmul  12022  zlem1lt  12547  zltlem1  12548  negelrp  12944  ioon0  13291  fzn  13460  fzrev2  13508  fz1sbc  13520  elfzp1b  13521  sumsqeq0  14106  fz1isolem  14388  sqrtle  15187  absgt0  15252  isershft  15591  incexc2  15765  dvdssubr  16236  gcdn0gt0  16449  divgcdcoprmex  16597  pcfac  16831  ramval  16940  isrnghm  20381  isorng  20798  iunocv  21640  ltbwe  22003  lmbrf  23208  perfcls  23313  ovolscalem1  25474  itg2mulclem  25707  sineq0  26493  efif1olem4  26514  logge0b  26600  loggt0b  26601  logle1b  26602  loglt1b  26603  atanord  26897  rlimcnp2  26936  bposlem7  27261  lgsprme0  27310  rpvmasum2  27483  sltsubsub2bd  28066  posdifsd  28080  sltmuldivwd  28183  onsbnd2  28263  pw2gt0divsd  28424  pw2ge0divsd  28425  pw2sltdiv1d  28431  zs12bdaylem1  28449  elreno2  28474  trgcgrg  28570  legov3  28653  opphllem6  28807  ebtwntg  29038  wwlksm1edg  29937  clwlkclwwlk2  30061  hial2eq2  31165  adjsym  31891  cnvadj  31950  eigvalcl  32019  mddmd  32359  mdslmd2i  32388  elat2  32398  indpreima  32928  xdivpnfrp  32995  ply1dg1rt  33642  unitdivcld  34039  ioosconn  35422  poimirlem26  37818  areacirclem1  37880  isat3  39604  ishlat3N  39651  cvrval5  39712  llnexchb2  40166  lhpoc2N  40312  lhprelat3N  40337  lautcnvle  40386  lautcvr  40389  ltrncnvatb  40435  cdlemb3  40903  cdlemg17h  40965  dih0vbN  41579  djhcvat42  41712  dvh4dimat  41735  mapdordlem2  41934  aks6d1c5lem1  42427  f1o2d2  42526  eluzp1  42598  reltsub1  42677  reltsubadd2  42678  sn-ltmul2d  42764  fsuppind  42869  diophun  43051  jm2.19lem4  43270  ordeldifsucon  43537  orddif0suc  43546  uneqsn  44302  xrralrecnnge  45670  limsupre2lem  46004  modmkpkne  47643  prprelb  47798  flsqrt5  47876  lincfsuppcl  48695