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  836  biassdc  1440  pm5.24dc  1443  anxordi  1445  sbequ12a  1821  drex1  1846  sbcomxyyz  2025  sb9v  2031  csbiebt  3168  prsspwg  3838  ssprss  3839  bnd2  4269  copsex2t  4343  copsex2g  4344  fnssresb  5451  fcnvres  5528  foelcdmi  5707  dmfco  5723  funimass5  5773  fmptco  5821  cbvfo  5936  cbvexfo  5937  isocnv  5962  isoini  5969  isoselem  5971  riota2df  6003  ovmpodxf  6157  caovcanrd  6196  suppimacnvfn  6424  fidcenumlemrks  7195  ordiso2  7277  ltpiord  7582  dfplpq2  7617  dfmpq2  7618  enqeceq  7622  enq0eceq  7700  enreceq  7999  ltpsrprg  8066  mappsrprg  8067  cnegexlem3  8398  subeq0  8447  negcon1  8473  subexsub  8593  subeqrev  8597  lesub  8663  ltsub13  8665  subge0  8697  div11ap  8922  divmuleqap  8939  ltmuldiv2  9097  lemuldiv2  9104  nn1suc  9204  addltmul  9423  elnnnn0  9487  znn0sub  9589  prime  9623  indstr  9871  qapne  9917  qlttri2  9919  fz1n  10324  fzrev3  10367  fzo0n  10448  fzonlt0  10449  divfl0  10602  modqsubdir  10701  fzfig  10738  wrdlenge1n0  11196  pfxccat3a  11368  sqrt11  11662  sqrtsq2  11666  absdiflt  11715  absdifle  11716  nnabscl  11723  minclpr  11860  xrnegiso  11885  xrnegcon1d  11887  clim2  11906  climshft2  11929  sumrbdc  12003  prodrbdclem2  12197  fprodssdc  12214  sinbnd  12376  cosbnd  12377  dvdscmulr  12444  dvdsmulcr  12445  oddm1even  12499  bitsmod  12580  bitsinv1lem  12585  qredeq  12731  cncongr2  12739  isprm3  12753  prmrp  12780  sqrt2irr  12797  crth  12859  pcdvdsb  12956  ssnnctlemct  13130  pwselbasb  13439  xpsfrnel2  13492  gsumval2  13543  imasmnd2  13598  grpid  13685  grpidrcan  13711  grpidlcan  13712  grplmulf1o  13720  imasgrp2  13760  ghmeqker  13921  abladdsub4  13964  imasrng  14033  imasring  14141  lspsnss2  14498  znf1o  14730  znidom  14736  znunit  14738  znrrg  14739  eltg3  14851  eltop  14863  eltop2  14864  eltop3  14865  lmbrf  15009  cncnpi  15022  txcn  15069  hmeoimaf1o  15108  ismet2  15148  xmseq0  15262  wilthlem1  15777  fsumdvdsmul  15788  lgsne0  15840  lgsquadlem1  15879  lgsquadlem2  15880  2sqlem7  15923  clwwlkn1  16342  eupth2lem2dc  16383  eupth2lem3lem3fi  16394  eupth2lem3lem6fi  16395