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  1787  drex1  1812  sbcomxyyz  1991  sb9v  1997  csbiebt  3124  prsspwg  3782  bnd2  4206  copsex2t  4278  copsex2g  4279  fnssresb  5370  fcnvres  5441  foelcdmi  5613  dmfco  5629  funimass5  5679  fmptco  5728  cbvfo  5832  cbvexfo  5833  isocnv  5858  isoini  5865  isoselem  5867  riota2df  5898  ovmpodxf  6048  caovcanrd  6087  fidcenumlemrks  7019  ordiso2  7101  ltpiord  7386  dfplpq2  7421  dfmpq2  7422  enqeceq  7426  enq0eceq  7504  enreceq  7803  ltpsrprg  7870  mappsrprg  7871  cnegexlem3  8203  subeq0  8252  negcon1  8278  subexsub  8398  subeqrev  8402  lesub  8468  ltsub13  8470  subge0  8502  div11ap  8727  divmuleqap  8744  ltmuldiv2  8902  lemuldiv2  8909  nn1suc  9009  addltmul  9228  elnnnn0  9292  znn0sub  9391  prime  9425  indstr  9667  qapne  9713  qlttri2  9715  fz1n  10119  fzrev3  10162  fzonlt0  10243  divfl0  10386  modqsubdir  10485  fzfig  10522  wrdlenge1n0  10968  sqrt11  11204  sqrtsq2  11208  absdiflt  11257  absdifle  11258  nnabscl  11265  minclpr  11402  xrnegiso  11427  xrnegcon1d  11429  clim2  11448  climshft2  11471  sumrbdc  11544  prodrbdclem2  11738  fprodssdc  11755  sinbnd  11917  cosbnd  11918  dvdscmulr  11985  dvdsmulcr  11986  oddm1even  12040  qredeq  12264  cncongr2  12272  isprm3  12286  prmrp  12313  sqrt2irr  12330  crth  12392  pcdvdsb  12489  ssnnctlemct  12663  xpsfrnel2  12989  gsumval2  13040  grpid  13171  grpidrcan  13197  grpidlcan  13198  grplmulf1o  13206  imasgrp2  13240  ghmeqker  13401  abladdsub4  13444  imasrng  13512  imasring  13620  lspsnss2  13975  znf1o  14207  znidom  14213  znunit  14215  znrrg  14216  eltg3  14293  eltop  14305  eltop2  14306  eltop3  14307  lmbrf  14451  cncnpi  14464  txcn  14511  hmeoimaf1o  14550  ismet2  14590  xmseq0  14704  wilthlem1  15216  fsumdvdsmul  15227  lgsne0  15279  lgsquadlem1  15318  lgsquadlem2  15319  2sqlem7  15362