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  840  biassdc  1444  pm5.24dc  1447  anxordi  1449  sbequ12a  1826  drex1  1851  sbcomxyyz  2032  sb9v  2038  csbiebt  3187  prsspwg  3873  ssprss  3874  bnd2  4308  copsex2t  4383  copsex2g  4384  fnssresb  5493  fcnvres  5573  foelcdmi  5752  dmfco  5770  funimass5  5820  fmptco  5868  cbvfo  5985  cbvexfo  5986  isocnv  6011  isoini  6018  isoselem  6020  riota2df  6054  ovmpodxf  6208  caovcanrd  6247  suppimacnvfn  6480  fidcenumlemrks  7264  ordiso2  7369  ltpiord  7680  dfplpq2  7715  dfmpq2  7716  enqeceq  7720  enq0eceq  7798  enreceq  8097  ltpsrprg  8164  mappsrprg  8165  cnegexlem3  8497  subeq0  8546  negcon1  8572  subexsub  8692  subeqrev  8696  lesub  8763  ltsub13  8765  subge0  8797  div11ap  9024  divmuleqap  9041  ltmuldiv2  9199  lemuldiv2  9206  nn1suc  9306  addltmul  9525  elnnnn0  9589  znn0sub  9693  prime  9728  indstr  9976  qapne  10022  qlttri2  10024  fz1n  10431  fzrev3  10477  fzo0n  10558  fzonlt0  10559  divfl0  10714  modqsubdir  10813  fzfig  10850  hashf1lem1  11268  wrdlenge1n0  11321  pfxccat3a  11493  sqrt11  11788  sqrtsq2  11792  absdiflt  11841  absdifle  11842  nnabscl  11849  minclpr  11986  xrnegiso  12011  xrnegcon1d  12013  clim2  12032  climshft2  12055  sumrbdc  12129  prodrbdclem2  12323  fprodssdc  12340  sinbnd  12502  cosbnd  12503  dvdscmulr  12570  dvdsmulcr  12571  oddm1even  12625  bitsmod  12706  bitsinv1lem  12711  qredeq  12857  cncongr2  12865  isprm3  12879  prmrp  12906  sqrt2irr  12923  crth  12985  pcdvdsb  13082  ballotfilemfc0  13215  ballotfilemfcc  13216  ssnnctlemct  13320  xpsfrnel2  13650  gzsumval2  13697  imasmnd2  13742  grpid  13827  grpidrcan  13853  grpidlcan  13854  grplmulf1o  13862  imasgrp2  13896  ghmeqker  14057  abladdsub4  14101  pwselbasb  14189  imasrng  14238  imasring  14352  lspsnss2  14739  znf1o  14969  znidom  14975  znunit  14977  znrrg  14978  eltg3  15141  eltop  15153  eltop2  15154  eltop3  15155  lmbrf  15299  cncnpi  15312  txcn  15359  hmeoimaf1o  15398  ismet2  15438  xmseq0  15552  wilthlem1  16077  fsumdvdsmul  16088  lgsne0  16140  lgsquadlem1  16179  lgsquadlem2  16180  2sqlem7  16223  clwwlkn1  16642  eupth2lem2dc  16683  eupth2lem3lem3fi  16694  eupth2lem3lem6fi  16695