Theorem bitr2d 268

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

Syntax hints:   → wi 4   ↔ wb 195

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 196

This theorem is referenced by:  3bitrrd  294  3bitr2rd  296  pm5.18  370  ifptru  1017  sbequ12a  2099  elrnmpt1  5295  fndmdif  6229  weniso  6504  sbcopeq1a  7111  cfss  8970  posdif  10400  lesub1  10401  lesub0  10424  possumd  10531  ltdivmul  10777  ledivmul  10778  zlem1lt  11306  zltlem1  11307  negelrp  11740  ioon0  12072  fzn  12228  fzrev2  12274  fz1sbc  12285  elfzp1b  12286  sumsqeq0  12804  fz1isolem  13102  sqrtle  13849  absgt0  13912  isershft  14242  incexc2  14409  dvdssubr  14865  gcdn0gt0  15077  divgcdcoprmex  15218  pcfac  15441  ramval  15550  ltbwe  19293  iunocv  19844  lmbrf  20874  perfcls  20979  ovolscalem1  23088  itg2mulclem  23319  sineq0  24077  efif1olem4  24095  atanord  24454  rlimcnp2  24493  bposlem7  24815  lgsprme0  24864  rpvmasum2  25001  trgcgrg  25210  legov3  25293  opphllem6  25444  ebtwntg  25662  wwlkm1edg  26263  usg2spthonot0  26416  hial2eq2  27348  adjsym  28076  cnvadj  28135  eigvalcl  28204  mddmd  28544  mdslmd2i  28573  elat2  28583  xdivpnfrp  28972  isorng  29130  unitdivcld  29275  indpreima  29414  iooscon  30483  pdivsq  30888  poimirlem26  32605  areacirclem1  32670  isat3  33612  ishlat3N  33659  cvrval5  33719  llnexchb2  34173  lhpoc2N  34319  lhprelat3N  34344  lautcnvle  34393  lautcvr  34396  ltrncnvatb  34442  cdlemb3  34912  cdlemg17h  34974  dih0vbN  35589  djhcvat42  35722  dvh4dimat  35745  mapdordlem2  35944  diophun  36355  jm2.19lem4  36577  uneqsn  37341  xrralrecnnge  38554  flsqrt5  40047  wwlksm1edg  41078  isrnghm  41682  lincfsuppcl  41996  logge0b  42123  loggt0b  42124  logle1b  42125  loglt1b  42126