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  818  biassdc  1385  pm5.24dc  1388  anxordi  1390  sbequ12a  1761  drex1  1786  sbcomxyyz  1960  sb9v  1966  csbiebt  3083  prsspwg  3731  bnd2  4151  copsex2t  4222  copsex2g  4223  fnssresb  5299  fcnvres  5370  dmfco  5553  funimass5  5601  fmptco  5650  cbvfo  5752  cbvexfo  5753  isocnv  5778  isoini  5785  isoselem  5787  riota2df  5817  ovmpodxf  5963  caovcanrd  6001  fidcenumlemrks  6914  ordiso2  6996  ltpiord  7256  dfplpq2  7291  dfmpq2  7292  enqeceq  7296  enq0eceq  7374  enreceq  7673  ltpsrprg  7740  mappsrprg  7741  cnegexlem3  8071  subeq0  8120  negcon1  8146  subexsub  8266  subeqrev  8270  lesub  8335  ltsub13  8337  subge0  8369  div11ap  8592  divmuleqap  8609  ltmuldiv2  8766  lemuldiv2  8773  nn1suc  8872  addltmul  9089  elnnnn0  9153  znn0sub  9252  prime  9286  indstr  9527  qapne  9573  qlttri2  9575  fz1n  9975  fzrev3  10018  fzonlt0  10098  divfl0  10227  modqsubdir  10324  fzfig  10361  sqrt11  10977  sqrtsq2  10981  absdiflt  11030  absdifle  11031  nnabscl  11038  minclpr  11174  xrnegiso  11199  xrnegcon1d  11201  clim2  11220  climshft2  11243  sumrbdc  11316  prodrbdclem2  11510  fprodssdc  11527  sinbnd  11689  cosbnd  11690  dvdscmulr  11756  dvdsmulcr  11757  oddm1even  11808  qredeq  12024  cncongr2  12032  isprm3  12046  prmrp  12073  sqrt2irr  12090  crth  12152  pcdvdsb  12247  ssnnctlemct  12375  eltg3  12657  eltop  12669  eltop2  12670  eltop3  12671  lmbrf  12815  cncnpi  12828  txcn  12875  hmeoimaf1o  12914  ismet2  12954  xmseq0  13068  lgsne0  13539  2sqlem7  13557