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-1 5  ax-2 6  ax-mp 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  774  biassdc  1332  pm5.24dc  1335  anxordi  1337  sbequ12a  1704  drex1  1727  sbcomxyyz  1895  sb9v  1903  csbiebt  2968  prsspwg  3602  bnd2  4014  copsex2t  4081  copsex2g  4082  fnssresb  5139  fcnvres  5207  dmfco  5385  funimass5  5430  fmptco  5478  cbvfo  5578  cbvexfo  5579  isocnv  5604  isoini  5611  isoselem  5613  riota2df  5642  ovmpt2dxf  5784  caovcanrd  5822  fidcenumlemrks  6716  ordiso2  6782  ltpiord  6939  dfplpq2  6974  dfmpq2  6975  enqeceq  6979  enq0eceq  7057  enreceq  7343  cnegexlem3  7720  subeq0  7769  negcon1  7795  subexsub  7911  subeqrev  7915  lesub  7980  ltsub13  7982  subge0  8014  div11ap  8228  divmuleqap  8245  ltmuldiv2  8397  lemuldiv2  8404  nn1suc  8502  addltmul  8713  elnnnn0  8777  znn0sub  8876  prime  8906  indstr  9142  qapne  9185  qlttri2  9187  fz1n  9519  fzrev3  9562  fzonlt0  9639  divfl0  9764  modqsubdir  9861  fzfig  9898  sqrt11  10533  sqrtsq2  10537  absdiflt  10586  absdifle  10587  nnabscl  10594  clim2  10732  climshft2  10756  isumrb  10829  sinbnd  11104  cosbnd  11105  dvdscmulr  11164  dvdsmulcr  11165  oddm1even  11214  qredeq  11417  cncongr2  11425  isprm3  11439  prmrp  11463  sqrt2irr  11480  crth  11539  eltg3  11818  eltop  11830  eltop2  11831  eltop3  11832