Theorem bitr3d 188

Description: Deduction form of bitr3i 184. (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 139	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜓))
3		bitr3d.2	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4	2, 3	bitrd 186	1 ⊢ (𝜑 → (𝜒 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 103

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  3bitrrd  213  3bitr3d  216  3bitr3rd  217  pm5.16  771  biassdc  1329  pm5.24dc  1332  anxordi  1334  sbequ12a  1700  drex1  1723  sbcomxyyz  1891  sb9v  1899  csbiebt  2956  prsspwg  3581  bnd2  3985  copsex2t  4048  copsex2g  4049  fnssresb  5093  fcnvres  5159  dmfco  5337  funimass5  5381  fmptco  5429  cbvfo  5527  cbvexfo  5528  isocnv  5553  isoini  5560  isoselem  5562  riota2df  5591  ovmpt2dxf  5729  caovcanrd  5767  ordiso2  6675  ltpiord  6825  dfplpq2  6860  dfmpq2  6861  enqeceq  6865  enq0eceq  6943  enreceq  7229  cnegexlem3  7606  subeq0  7655  negcon1  7681  subexsub  7797  subeqrev  7801  lesub  7866  ltsub13  7868  subge0  7900  div11ap  8109  divmuleqap  8126  ltmuldiv2  8274  lemuldiv2  8281  nn1suc  8379  addltmul  8588  elnnnn0  8652  znn0sub  8751  prime  8781  indstr  9016  qapne  9059  qlttri2  9061  fz1n  9393  fzrev3  9434  fzonlt0  9509  divfl0  9634  modqsubdir  9731  fzfig  9768  sqrt11  10371  sqrtsq2  10375  absdiflt  10424  absdifle  10425  nnabscl  10432  clim2  10569  climshft2  10592  isumrb  10662  dvdscmulr  10731  dvdsmulcr  10732  oddm1even  10781  qredeq  10984  cncongr2  10992  isprm3  11006  prmrp  11030  sqrt2irr  11047  crth  11106