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  1406  pm5.24dc  1409  anxordi  1411  sbequ12a  1784  drex1  1809  sbcomxyyz  1984  sb9v  1990  csbiebt  3111  prsspwg  3767  bnd2  4188  copsex2t  4260  copsex2g  4261  fnssresb  5344  fcnvres  5415  foelcdmi  5585  dmfco  5601  funimass5  5650  fmptco  5699  cbvfo  5803  cbvexfo  5804  isocnv  5829  isoini  5836  isoselem  5838  riota2df  5868  ovmpodxf  6018  caovcanrd  6056  fidcenumlemrks  6972  ordiso2  7054  ltpiord  7338  dfplpq2  7373  dfmpq2  7374  enqeceq  7378  enq0eceq  7456  enreceq  7755  ltpsrprg  7822  mappsrprg  7823  cnegexlem3  8154  subeq0  8203  negcon1  8229  subexsub  8349  subeqrev  8353  lesub  8418  ltsub13  8420  subge0  8452  div11ap  8677  divmuleqap  8694  ltmuldiv2  8852  lemuldiv2  8859  nn1suc  8958  addltmul  9175  elnnnn0  9239  znn0sub  9338  prime  9372  indstr  9613  qapne  9659  qlttri2  9661  fz1n  10064  fzrev3  10107  fzonlt0  10187  divfl0  10316  modqsubdir  10413  fzfig  10450  sqrt11  11068  sqrtsq2  11072  absdiflt  11121  absdifle  11122  nnabscl  11129  minclpr  11265  xrnegiso  11290  xrnegcon1d  11292  clim2  11311  climshft2  11334  sumrbdc  11407  prodrbdclem2  11601  fprodssdc  11618  sinbnd  11780  cosbnd  11781  dvdscmulr  11847  dvdsmulcr  11848  oddm1even  11900  qredeq  12116  cncongr2  12124  isprm3  12138  prmrp  12165  sqrt2irr  12182  crth  12244  pcdvdsb  12339  ssnnctlemct  12472  xpsfrnel2  12795  grpid  12956  grpidrcan  12982  grpidlcan  12983  grplmulf1o  12991  imasgrp2  13025  ghmeqker  13178  abladdsub4  13221  imasrng  13278  imasring  13382  lspsnss2  13703  eltg3  13961  eltop  13973  eltop2  13974  eltop3  13975  lmbrf  14119  cncnpi  14132  txcn  14179  hmeoimaf1o  14218  ismet2  14258  xmseq0  14372  lgsne0  14843  2sqlem7  14872