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  833  biassdc  1437  pm5.24dc  1440  anxordi  1442  sbequ12a  1819  drex1  1844  sbcomxyyz  2023  sb9v  2029  csbiebt  3165  prsspwg  3831  ssprss  3832  bnd2  4261  copsex2t  4335  copsex2g  4336  fnssresb  5441  fcnvres  5517  foelcdmi  5694  dmfco  5710  funimass5  5760  fmptco  5809  cbvfo  5921  cbvexfo  5922  isocnv  5947  isoini  5954  isoselem  5956  riota2df  5988  ovmpodxf  6142  caovcanrd  6181  fidcenumlemrks  7146  ordiso2  7228  ltpiord  7532  dfplpq2  7567  dfmpq2  7568  enqeceq  7572  enq0eceq  7650  enreceq  7949  ltpsrprg  8016  mappsrprg  8017  cnegexlem3  8349  subeq0  8398  negcon1  8424  subexsub  8544  subeqrev  8548  lesub  8614  ltsub13  8616  subge0  8648  div11ap  8873  divmuleqap  8890  ltmuldiv2  9048  lemuldiv2  9055  nn1suc  9155  addltmul  9374  elnnnn0  9438  znn0sub  9538  prime  9572  indstr  9820  qapne  9866  qlttri2  9868  fz1n  10272  fzrev3  10315  fzo0n  10396  fzonlt0  10397  divfl0  10549  modqsubdir  10648  fzfig  10685  wrdlenge1n0  11140  pfxccat3a  11312  sqrt11  11593  sqrtsq2  11597  absdiflt  11646  absdifle  11647  nnabscl  11654  minclpr  11791  xrnegiso  11816  xrnegcon1d  11818  clim2  11837  climshft2  11860  sumrbdc  11933  prodrbdclem2  12127  fprodssdc  12144  sinbnd  12306  cosbnd  12307  dvdscmulr  12374  dvdsmulcr  12375  oddm1even  12429  bitsmod  12510  bitsinv1lem  12515  qredeq  12661  cncongr2  12669  isprm3  12683  prmrp  12710  sqrt2irr  12727  crth  12789  pcdvdsb  12886  ssnnctlemct  13060  pwselbasb  13369  xpsfrnel2  13422  gsumval2  13473  imasmnd2  13528  grpid  13615  grpidrcan  13641  grpidlcan  13642  grplmulf1o  13650  imasgrp2  13690  ghmeqker  13851  abladdsub4  13894  imasrng  13962  imasring  14070  lspsnss2  14426  znf1o  14658  znidom  14664  znunit  14666  znrrg  14667  eltg3  14774  eltop  14786  eltop2  14787  eltop3  14788  lmbrf  14932  cncnpi  14945  txcn  14992  hmeoimaf1o  15031  ismet2  15071  xmseq0  15185  wilthlem1  15697  fsumdvdsmul  15708  lgsne0  15760  lgsquadlem1  15799  lgsquadlem2  15800  2sqlem7  15843  clwwlkn1  16227