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  828  biassdc  1395  pm5.24dc  1398  anxordi  1400  sbequ12a  1771  drex1  1796  sbcomxyyz  1970  sb9v  1976  csbiebt  3094  prsspwg  3748  bnd2  4168  copsex2t  4239  copsex2g  4240  fnssresb  5320  fcnvres  5391  foelcdmi  5560  dmfco  5576  funimass5  5625  fmptco  5674  cbvfo  5776  cbvexfo  5777  isocnv  5802  isoini  5809  isoselem  5811  riota2df  5841  ovmpodxf  5990  caovcanrd  6028  fidcenumlemrks  6942  ordiso2  7024  ltpiord  7293  dfplpq2  7328  dfmpq2  7329  enqeceq  7333  enq0eceq  7411  enreceq  7710  ltpsrprg  7777  mappsrprg  7778  cnegexlem3  8108  subeq0  8157  negcon1  8183  subexsub  8303  subeqrev  8307  lesub  8372  ltsub13  8374  subge0  8406  div11ap  8629  divmuleqap  8646  ltmuldiv2  8803  lemuldiv2  8810  nn1suc  8909  addltmul  9126  elnnnn0  9190  znn0sub  9289  prime  9323  indstr  9564  qapne  9610  qlttri2  9612  fz1n  10012  fzrev3  10055  fzonlt0  10135  divfl0  10264  modqsubdir  10361  fzfig  10398  sqrt11  11014  sqrtsq2  11018  absdiflt  11067  absdifle  11068  nnabscl  11075  minclpr  11211  xrnegiso  11236  xrnegcon1d  11238  clim2  11257  climshft2  11280  sumrbdc  11353  prodrbdclem2  11547  fprodssdc  11564  sinbnd  11726  cosbnd  11727  dvdscmulr  11793  dvdsmulcr  11794  oddm1even  11845  qredeq  12061  cncongr2  12069  isprm3  12083  prmrp  12110  sqrt2irr  12127  crth  12189  pcdvdsb  12284  ssnnctlemct  12412  grpid  12772  grpidrcan  12794  grpidlcan  12795  grplmulf1o  12803  abladdsub4  12913  eltg3  13108  eltop  13120  eltop2  13121  eltop3  13122  lmbrf  13266  cncnpi  13279  txcn  13326  hmeoimaf1o  13365  ismet2  13405  xmseq0  13519  lgsne0  13990  2sqlem7  14008