Theorem bitr3d 189

Description: Deduction form of bitr3i 185. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
bitr3d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
bitr3d.2	⊢ (𝜑 → (𝜓 ↔ 𝜃))

Assertion

Ref	Expression
bitr3d	⊢ (𝜑 → (𝜒 ↔ 𝜃))

Proof of Theorem bitr3d

Step	Hyp	Ref	Expression
1		bitr3d.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	bicomd 140	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜓))
3		bitr3d.2	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4	2, 3	bitrd 187	1 ⊢ (𝜑 → (𝜒 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3bitrrd  214  3bitr3d  217  3bitr3rd  218  pm5.16  814  biassdc  1374  pm5.24dc  1377  anxordi  1379  sbequ12a  1747  drex1  1771  sbcomxyyz  1946  sb9v  1954  csbiebt  3044  prsspwg  3687  bnd2  4105  copsex2t  4175  copsex2g  4176  fnssresb  5243  fcnvres  5314  dmfco  5497  funimass5  5545  fmptco  5594  cbvfo  5694  cbvexfo  5695  isocnv  5720  isoini  5727  isoselem  5729  riota2df  5758  ovmpodxf  5904  caovcanrd  5942  fidcenumlemrks  6849  ordiso2  6928  ltpiord  7151  dfplpq2  7186  dfmpq2  7187  enqeceq  7191  enq0eceq  7269  enreceq  7568  ltpsrprg  7635  mappsrprg  7636  cnegexlem3  7963  subeq0  8012  negcon1  8038  subexsub  8158  subeqrev  8162  lesub  8227  ltsub13  8229  subge0  8261  div11ap  8484  divmuleqap  8501  ltmuldiv2  8657  lemuldiv2  8664  nn1suc  8763  addltmul  8980  elnnnn0  9044  znn0sub  9143  prime  9174  indstr  9415  qapne  9458  qlttri2  9460  fz1n  9855  fzrev3  9898  fzonlt0  9975  divfl0  10100  modqsubdir  10197  fzfig  10234  sqrt11  10843  sqrtsq2  10847  absdiflt  10896  absdifle  10897  nnabscl  10904  minclpr  11040  xrnegiso  11063  xrnegcon1d  11065  clim2  11084  climshft2  11107  sumrbdc  11180  prodrbdclem2  11374  sinbnd  11495  cosbnd  11496  dvdscmulr  11558  dvdsmulcr  11559  oddm1even  11608  qredeq  11813  cncongr2  11821  isprm3  11835  prmrp  11859  sqrt2irr  11876  crth  11936  eltg3  12265  eltop  12277  eltop2  12278  eltop3  12279  lmbrf  12423  cncnpi  12436  txcn  12483  hmeoimaf1o  12522  ismet2  12562  xmseq0  12676