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  6977  ordiso2  7059  ltpiord  7343  dfplpq2  7378  dfmpq2  7379  enqeceq  7383  enq0eceq  7461  enreceq  7760  ltpsrprg  7827  mappsrprg  7828  cnegexlem3  8159  subeq0  8208  negcon1  8234  subexsub  8354  subeqrev  8358  lesub  8423  ltsub13  8425  subge0  8457  div11ap  8682  divmuleqap  8699  ltmuldiv2  8857  lemuldiv2  8864  nn1suc  8963  addltmul  9180  elnnnn0  9244  znn0sub  9343  prime  9377  indstr  9618  qapne  9664  qlttri2  9666  fz1n  10069  fzrev3  10112  fzonlt0  10192  divfl0  10322  modqsubdir  10419  fzfig  10456  sqrt11  11075  sqrtsq2  11079  absdiflt  11128  absdifle  11129  nnabscl  11136  minclpr  11272  xrnegiso  11297  xrnegcon1d  11299  clim2  11318  climshft2  11341  sumrbdc  11414  prodrbdclem2  11608  fprodssdc  11625  sinbnd  11787  cosbnd  11788  dvdscmulr  11854  dvdsmulcr  11855  oddm1even  11907  qredeq  12123  cncongr2  12131  isprm3  12145  prmrp  12172  sqrt2irr  12189  crth  12251  pcdvdsb  12347  ssnnctlemct  12492  xpsfrnel2  12815  grpid  12976  grpidrcan  13002  grpidlcan  13003  grplmulf1o  13011  imasgrp2  13045  ghmeqker  13203  abladdsub4  13246  imasrng  13303  imasring  13407  lspsnss2  13728  eltg3  13994  eltop  14006  eltop2  14007  eltop3  14008  lmbrf  14152  cncnpi  14165  txcn  14212  hmeoimaf1o  14251  ismet2  14291  xmseq0  14405  lgsne0  14876  2sqlem7  14905