Theorem bitr3d 190

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

Syntax hints:   → wi 4   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3bitrrd  215  3bitr3d  218  3bitr3rd  219  pm5.16  830  biassdc  1415  pm5.24dc  1418  anxordi  1420  sbequ12a  1797  drex1  1822  sbcomxyyz  2001  sb9v  2007  csbiebt  3134  prsspwg  3795  bnd2  4221  copsex2t  4293  copsex2g  4294  fnssresb  5393  fcnvres  5466  foelcdmi  5638  dmfco  5654  funimass5  5704  fmptco  5753  cbvfo  5861  cbvexfo  5862  isocnv  5887  isoini  5894  isoselem  5896  riota2df  5927  ovmpodxf  6078  caovcanrd  6117  fidcenumlemrks  7062  ordiso2  7144  ltpiord  7439  dfplpq2  7474  dfmpq2  7475  enqeceq  7479  enq0eceq  7557  enreceq  7856  ltpsrprg  7923  mappsrprg  7924  cnegexlem3  8256  subeq0  8305  negcon1  8331  subexsub  8451  subeqrev  8455  lesub  8521  ltsub13  8523  subge0  8555  div11ap  8780  divmuleqap  8797  ltmuldiv2  8955  lemuldiv2  8962  nn1suc  9062  addltmul  9281  elnnnn0  9345  znn0sub  9445  prime  9479  indstr  9721  qapne  9767  qlttri2  9769  fz1n  10173  fzrev3  10216  fzo0n  10297  fzonlt0  10298  divfl0  10446  modqsubdir  10545  fzfig  10582  wrdlenge1n0  11034  sqrt11  11394  sqrtsq2  11398  absdiflt  11447  absdifle  11448  nnabscl  11455  minclpr  11592  xrnegiso  11617  xrnegcon1d  11619  clim2  11638  climshft2  11661  sumrbdc  11734  prodrbdclem2  11928  fprodssdc  11945  sinbnd  12107  cosbnd  12108  dvdscmulr  12175  dvdsmulcr  12176  oddm1even  12230  bitsmod  12311  bitsinv1lem  12316  qredeq  12462  cncongr2  12470  isprm3  12484  prmrp  12511  sqrt2irr  12528  crth  12590  pcdvdsb  12687  ssnnctlemct  12861  pwselbasb  13169  xpsfrnel2  13222  gsumval2  13273  imasmnd2  13328  grpid  13415  grpidrcan  13441  grpidlcan  13442  grplmulf1o  13450  imasgrp2  13490  ghmeqker  13651  abladdsub4  13694  imasrng  13762  imasring  13870  lspsnss2  14225  znf1o  14457  znidom  14463  znunit  14465  znrrg  14466  eltg3  14573  eltop  14585  eltop2  14586  eltop3  14587  lmbrf  14731  cncnpi  14744  txcn  14791  hmeoimaf1o  14830  ismet2  14870  xmseq0  14984  wilthlem1  15496  fsumdvdsmul  15507  lgsne0  15559  lgsquadlem1  15598  lgsquadlem2  15599  2sqlem7  15642