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 ⊢ (𝜑 → (𝜒 ↔ 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used 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  3875  ssprss  3876  bnd2  4312  copsex2t  4387  copsex2g  4388  fnssresb  5498  fcnvres  5578  foelcdmi  5758  dmfco  5776  funimass5  5829  fmptco  5877  cbvfo  5994  cbvexfo  5995  isocnv  6020  isoini  6027  isoselem  6029  riota2df  6063  ovmpodxf  6217  caovcanrd  6256  suppimacnvfn  6490  fidcenumlemrks  7277  ordiso2  7381  ltpiord  7692  dfplpq2  7727  dfmpq2  7728  enqeceq  7732  enq0eceq  7810  enreceq  8109  ltpsrprg  8176  mappsrprg  8177  cnegexlem3  8510  subeq0  8559  negcon1  8585  subexsub  8705  subeqrev  8709  lesub  8776  ltsub13  8778  subge0  8810  div11ap  9038  divmuleqap  9055  ltmuldiv2  9213  lemuldiv2  9220  nn1suc  9332  addltmul  9553  elnnnn0  9617  znn0sub  9719  prime  9755  indstr  10008  qapne  10054  qlttri2  10056  fz1n  10464  fzrev3  10510  fzo0n  10591  fzonlt0  10592  divfl0  10751  modqsubdir  10850  fzfig  10887  hashf1lem1  11306  wrdlenge1n0  11359  pfxccat3a  11531  sqrt11  11826  sqrtsq2  11830  absdiflt  11880  absdifle  11881  nnabscl  11888  minclpr  12026  xrnegiso  12052  xrnegcon1d  12054  clim2  12073  climshft2  12096  sumrbdc  12170  prodrbdclem2  12364  fprodssdc  12381  sinbnd  12543  cosbnd  12544  dvdscmulr  12611  dvdsmulcr  12612  oddm1even  12666  bitsmod  12747  bitsinv1lem  12752  qredeq  12898  cncongr2  12906  isprm3  12920  prmrp  12948  sqrt2irr  12965  crth  13030  pcdvdsb  13127  ballotfilemfc0  13289  ballotfilemfcc  13290  ssnnctlemct  13394  xpsfrnel2  13725  gzsumval2  13772  imasmnd2  13817  grpid  13902  grpidrcan  13928  grpidlcan  13929  grplmulf1o  13937  imasgrp2  13971  ghmeqker  14132  abladdsub4  14207  pwselbasb  14312  imasrng  14361  imasring  14477  lspsnss2  14864  znf1o  15094  znidom  15100  znunit  15102  znrrg  15103  gsumbagdiaglem  15184  eltg3  15300  eltop  15312  eltop2  15313  eltop3  15314  lmbrf  15458  cncnpi  15471  txcn  15518  hmeoimaf1o  15557  ismet2  15597  xmseq0  15711  wilthlem1  16249  fsumdvdsmul  16302  lgsne0  16379  lgsquadlem1  16418  lgsquadlem2  16419  2sqlem7  16462  clwwlkn1  16881  eupth2lem2dc  16922  eupth2lem3lem3fi  16933  eupth2lem3lem6fi  16934