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  1988  sb9v  1994  csbiebt  3121  prsspwg  3779  bnd2  4203  copsex2t  4275  copsex2g  4276  fnssresb  5367  fcnvres  5438  foelcdmi  5610  dmfco  5626  funimass5  5676  fmptco  5725  cbvfo  5829  cbvexfo  5830  isocnv  5855  isoini  5862  isoselem  5864  riota2df  5895  ovmpodxf  6045  caovcanrd  6084  fidcenumlemrks  7014  ordiso2  7096  ltpiord  7381  dfplpq2  7416  dfmpq2  7417  enqeceq  7421  enq0eceq  7499  enreceq  7798  ltpsrprg  7865  mappsrprg  7866  cnegexlem3  8198  subeq0  8247  negcon1  8273  subexsub  8393  subeqrev  8397  lesub  8462  ltsub13  8464  subge0  8496  div11ap  8721  divmuleqap  8738  ltmuldiv2  8896  lemuldiv2  8903  nn1suc  9003  addltmul  9222  elnnnn0  9286  znn0sub  9385  prime  9419  indstr  9661  qapne  9707  qlttri2  9709  fz1n  10113  fzrev3  10156  fzonlt0  10237  divfl0  10368  modqsubdir  10467  fzfig  10504  wrdlenge1n0  10950  sqrt11  11186  sqrtsq2  11190  absdiflt  11239  absdifle  11240  nnabscl  11247  minclpr  11383  xrnegiso  11408  xrnegcon1d  11410  clim2  11429  climshft2  11452  sumrbdc  11525  prodrbdclem2  11719  fprodssdc  11736  sinbnd  11898  cosbnd  11899  dvdscmulr  11966  dvdsmulcr  11967  oddm1even  12019  qredeq  12237  cncongr2  12245  isprm3  12259  prmrp  12286  sqrt2irr  12303  crth  12365  pcdvdsb  12461  ssnnctlemct  12606  xpsfrnel2  12932  gsumval2  12983  grpid  13114  grpidrcan  13140  grpidlcan  13141  grplmulf1o  13149  imasgrp2  13183  ghmeqker  13344  abladdsub4  13387  imasrng  13455  imasring  13563  lspsnss2  13918  znf1o  14150  znidom  14156  znunit  14158  znrrg  14159  eltg3  14236  eltop  14248  eltop2  14249  eltop3  14250  lmbrf  14394  cncnpi  14407  txcn  14454  hmeoimaf1o  14493  ismet2  14533  xmseq0  14647  wilthlem1  15153  lgsne0  15195  lgsquadlem1  15234  lgsquadlem2  15235  2sqlem7  15278