Theorem bitr2d 279

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  3bitrrd  306  3bitr2rd  308  pm5.18  383  ifptru  1073  sbequ12a  2248  elrnmpt1  5870  fndmdif  6928  weniso  7234  sbcopeq1a  7899  snmapen  8837  dmttrcl  9488  cfss  10030  posdif  11477  lesub1  11478  lesub0  11501  possumd  11609  ltdivmul  11859  ledivmul  11860  zlem1lt  12381  zltlem1  12382  negelrp  12772  ioon0  13114  fzn  13281  fzrev2  13329  fz1sbc  13341  elfzp1b  13342  sumsqeq0  13905  fz1isolem  14184  sqrtle  14981  absgt0  15045  isershft  15384  incexc2  15559  dvdssubr  16023  gcdn0gt0  16234  divgcdcoprmex  16380  prmdvdssqOLD  16433  pcfac  16609  ramval  16718  iunocv  20895  ltbwe  21254  lmbrf  22420  perfcls  22525  ovolscalem1  24686  itg2mulclem  24920  sineq0  25689  efif1olem4  25710  logge0b  25795  loggt0b  25796  logle1b  25797  loglt1b  25798  atanord  26086  rlimcnp2  26125  bposlem7  26447  lgsprme0  26496  rpvmasum2  26669  trgcgrg  26885  legov3  26968  opphllem6  27122  ebtwntg  27359  wwlksm1edg  28255  clwlkclwwlk2  28376  hial2eq2  29478  adjsym  30204  cnvadj  30263  eigvalcl  30332  mddmd  30672  mdslmd2i  30701  elat2  30711  xdivpnfrp  31216  isorng  31507  unitdivcld  31860  indpreima  32002  ioosconn  33218  xpord2pred  33801  xpord3pred  33807  poimirlem26  35812  areacirclem1  35874  isat3  37328  ishlat3N  37375  cvrval5  37436  llnexchb2  37890  lhpoc2N  38036  lhprelat3N  38061  lautcnvle  38110  lautcvr  38113  ltrncnvatb  38159  cdlemb3  38627  cdlemg17h  38689  dih0vbN  39303  djhcvat42  39436  dvh4dimat  39459  mapdordlem2  39658  fsuppind  40286  reltsub1  40376  reltsubadd2  40377  sn-ltmul2d  40438  diophun  40602  jm2.19lem4  40821  uneqsn  41640  xrralrecnnge  42937  limsupre2lem  43272  prprelb  44979  flsqrt5  45057  isrnghm  45461  lincfsuppcl  45765