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  813  biassdc  1373  pm5.24dc  1376  anxordi  1378  sbequ12a  1746  drex1  1770  sbcomxyyz  1945  sb9v  1953  csbiebt  3039  prsspwg  3679  bnd2  4097  copsex2t  4167  copsex2g  4168  fnssresb  5235  fcnvres  5306  dmfco  5489  funimass5  5537  fmptco  5586  cbvfo  5686  cbvexfo  5687  isocnv  5712  isoini  5719  isoselem  5721  riota2df  5750  ovmpodxf  5896  caovcanrd  5934  fidcenumlemrks  6841  ordiso2  6920  ltpiord  7127  dfplpq2  7162  dfmpq2  7163  enqeceq  7167  enq0eceq  7245  enreceq  7544  ltpsrprg  7611  mappsrprg  7612  cnegexlem3  7939  subeq0  7988  negcon1  8014  subexsub  8134  subeqrev  8138  lesub  8203  ltsub13  8205  subge0  8237  div11ap  8460  divmuleqap  8477  ltmuldiv2  8633  lemuldiv2  8640  nn1suc  8739  addltmul  8956  elnnnn0  9020  znn0sub  9119  prime  9150  indstr  9388  qapne  9431  qlttri2  9433  fz1n  9824  fzrev3  9867  fzonlt0  9944  divfl0  10069  modqsubdir  10166  fzfig  10203  sqrt11  10811  sqrtsq2  10815  absdiflt  10864  absdifle  10865  nnabscl  10872  minclpr  11008  xrnegiso  11031  xrnegcon1d  11033  clim2  11052  climshft2  11075  sumrbdc  11148  prodrbdclem2  11342  sinbnd  11459  cosbnd  11460  dvdscmulr  11522  dvdsmulcr  11523  oddm1even  11572  qredeq  11777  cncongr2  11785  isprm3  11799  prmrp  11823  sqrt2irr  11840  crth  11900  eltg3  12226  eltop  12238  eltop2  12239  eltop3  12240  lmbrf  12384  cncnpi  12397  txcn  12444  hmeoimaf1o  12483  ismet2  12523  xmseq0  12637