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  829  biassdc  1405  pm5.24dc  1408  anxordi  1410  sbequ12a  1783  drex1  1808  sbcomxyyz  1982  sb9v  1988  csbiebt  3108  prsspwg  3764  bnd2  4185  copsex2t  4257  copsex2g  4258  fnssresb  5340  fcnvres  5411  foelcdmi  5581  dmfco  5597  funimass5  5646  fmptco  5695  cbvfo  5799  cbvexfo  5800  isocnv  5825  isoini  5832  isoselem  5834  riota2df  5864  ovmpodxf  6014  caovcanrd  6052  fidcenumlemrks  6966  ordiso2  7048  ltpiord  7332  dfplpq2  7367  dfmpq2  7368  enqeceq  7372  enq0eceq  7450  enreceq  7749  ltpsrprg  7816  mappsrprg  7817  cnegexlem3  8148  subeq0  8197  negcon1  8223  subexsub  8343  subeqrev  8347  lesub  8412  ltsub13  8414  subge0  8446  div11ap  8671  divmuleqap  8688  ltmuldiv2  8846  lemuldiv2  8853  nn1suc  8952  addltmul  9169  elnnnn0  9233  znn0sub  9332  prime  9366  indstr  9607  qapne  9653  qlttri2  9655  fz1n  10058  fzrev3  10101  fzonlt0  10181  divfl0  10310  modqsubdir  10407  fzfig  10444  sqrt11  11062  sqrtsq2  11066  absdiflt  11115  absdifle  11116  nnabscl  11123  minclpr  11259  xrnegiso  11284  xrnegcon1d  11286  clim2  11305  climshft2  11328  sumrbdc  11401  prodrbdclem2  11595  fprodssdc  11612  sinbnd  11774  cosbnd  11775  dvdscmulr  11841  dvdsmulcr  11842  oddm1even  11894  qredeq  12110  cncongr2  12118  isprm3  12132  prmrp  12159  sqrt2irr  12176  crth  12238  pcdvdsb  12333  ssnnctlemct  12461  xpsfrnel2  12784  grpid  12936  grpidrcan  12962  grpidlcan  12963  grplmulf1o  12971  imasgrp2  13005  abladdsub4  13151  imasrng  13208  imasring  13312  lspsnss2  13608  eltg3  13853  eltop  13865  eltop2  13866  eltop3  13867  lmbrf  14011  cncnpi  14024  txcn  14071  hmeoimaf1o  14110  ismet2  14150  xmseq0  14264  lgsne0  14735  2sqlem7  14764