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  1074  sbequ12a  2256  elrnmpt1  5897  fndmdif  6970  weniso  7283  sbcopeq1a  7976  xpord2pred  8070  snmapen  8955  dmttrcl  9606  cfss  10148  posdif  11602  lesub1  11603  lesub0  11626  possumd  11734  ltdivmul  11989  ledivmul  11990  zlem1lt  12516  zltlem1  12517  negelrp  12917  ioon0  13263  fzn  13432  fzrev2  13480  fz1sbc  13492  elfzp1b  13493  sumsqeq0  14078  fz1isolem  14360  sqrtle  15159  absgt0  15224  isershft  15563  incexc2  15737  dvdssubr  16208  gcdn0gt0  16421  divgcdcoprmex  16569  pcfac  16803  ramval  16912  isrnghm  20352  isorng  20769  iunocv  21611  ltbwe  21972  lmbrf  23168  perfcls  23273  ovolscalem1  25434  itg2mulclem  25667  sineq0  26453  efif1olem4  26474  logge0b  26560  loggt0b  26561  logle1b  26562  loglt1b  26563  atanord  26857  rlimcnp2  26896  bposlem7  27221  lgsprme0  27270  rpvmasum2  27443  sltsubsub2bd  28017  posdifsd  28030  sltmuldivwd  28133  pw2gt0divsd  28361  pw2ge0divsd  28362  pw2sltdiv1d  28368  trgcgrg  28486  legov3  28569  opphllem6  28723  ebtwntg  28953  wwlksm1edg  29852  clwlkclwwlk2  29973  hial2eq2  31077  adjsym  31803  cnvadj  31862  eigvalcl  31931  mddmd  32271  mdslmd2i  32300  elat2  32310  indpreima  32836  xdivpnfrp  32903  ply1dg1rt  33533  unitdivcld  33904  ioosconn  35259  poimirlem26  37665  areacirclem1  37727  isat3  39325  ishlat3N  39372  cvrval5  39433  llnexchb2  39887  lhpoc2N  40033  lhprelat3N  40058  lautcnvle  40107  lautcvr  40110  ltrncnvatb  40156  cdlemb3  40624  cdlemg17h  40686  dih0vbN  41300  djhcvat42  41433  dvh4dimat  41456  mapdordlem2  41655  aks6d1c5lem1  42148  f1o2d2  42245  eluzp1  42319  reltsub1  42398  reltsubadd2  42399  sn-ltmul2d  42485  fsuppind  42602  diophun  42785  jm2.19lem4  43004  ordeldifsucon  43271  orddif0suc  43280  uneqsn  44037  xrralrecnnge  45407  limsupre2lem  45741  modmkpkne  47371  prprelb  47526  flsqrt5  47604  lincfsuppcl  48424