Theorem bitr3d 189

Description: Deduction form of bitr3i 185. (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 140	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜓))
3		bitr3d.2	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4	2, 3	bitrd 187	1 ⊢ (𝜑 → (𝜒 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3bitrrd  214  3bitr3d  217  3bitr3rd  218  pm5.16  823  biassdc  1390  pm5.24dc  1393  anxordi  1395  sbequ12a  1766  drex1  1791  sbcomxyyz  1965  sb9v  1971  csbiebt  3088  prsspwg  3739  bnd2  4159  copsex2t  4230  copsex2g  4231  fnssresb  5310  fcnvres  5381  dmfco  5564  funimass5  5613  fmptco  5662  cbvfo  5764  cbvexfo  5765  isocnv  5790  isoini  5797  isoselem  5799  riota2df  5829  ovmpodxf  5978  caovcanrd  6016  fidcenumlemrks  6930  ordiso2  7012  ltpiord  7281  dfplpq2  7316  dfmpq2  7317  enqeceq  7321  enq0eceq  7399  enreceq  7698  ltpsrprg  7765  mappsrprg  7766  cnegexlem3  8096  subeq0  8145  negcon1  8171  subexsub  8291  subeqrev  8295  lesub  8360  ltsub13  8362  subge0  8394  div11ap  8617  divmuleqap  8634  ltmuldiv2  8791  lemuldiv2  8798  nn1suc  8897  addltmul  9114  elnnnn0  9178  znn0sub  9277  prime  9311  indstr  9552  qapne  9598  qlttri2  9600  fz1n  10000  fzrev3  10043  fzonlt0  10123  divfl0  10252  modqsubdir  10349  fzfig  10386  sqrt11  11003  sqrtsq2  11007  absdiflt  11056  absdifle  11057  nnabscl  11064  minclpr  11200  xrnegiso  11225  xrnegcon1d  11227  clim2  11246  climshft2  11269  sumrbdc  11342  prodrbdclem2  11536  fprodssdc  11553  sinbnd  11715  cosbnd  11716  dvdscmulr  11782  dvdsmulcr  11783  oddm1even  11834  qredeq  12050  cncongr2  12058  isprm3  12072  prmrp  12099  sqrt2irr  12116  crth  12178  pcdvdsb  12273  ssnnctlemct  12401  grpid  12742  grpidrcan  12764  grpidlcan  12765  eltg3  12851  eltop  12863  eltop2  12864  eltop3  12865  lmbrf  13009  cncnpi  13022  txcn  13069  hmeoimaf1o  13108  ismet2  13148  xmseq0  13262  lgsne0  13733  2sqlem7  13751