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  4310  copsex2t  4385  copsex2g  4386  fnssresb  5495  fcnvres  5575  foelcdmi  5755  dmfco  5773  funimass5  5826  fmptco  5874  cbvfo  5991  cbvexfo  5992  isocnv  6017  isoini  6024  isoselem  6026  riota2df  6060  ovmpodxf  6214  caovcanrd  6253  suppimacnvfn  6486  fidcenumlemrks  7270  ordiso2  7375  ltpiord  7686  dfplpq2  7721  dfmpq2  7722  enqeceq  7726  enq0eceq  7804  enreceq  8103  ltpsrprg  8170  mappsrprg  8171  cnegexlem3  8503  subeq0  8552  negcon1  8578  subexsub  8698  subeqrev  8702  lesub  8769  ltsub13  8771  subge0  8803  div11ap  9031  divmuleqap  9048  ltmuldiv2  9206  lemuldiv2  9213  nn1suc  9324  addltmul  9544  elnnnn0  9608  znn0sub  9712  prime  9747  indstr  9995  qapne  10041  qlttri2  10043  fz1n  10450  fzrev3  10496  fzo0n  10577  fzonlt0  10578  divfl0  10733  modqsubdir  10832  fzfig  10869  hashf1lem1  11287  wrdlenge1n0  11340  pfxccat3a  11512  sqrt11  11807  sqrtsq2  11811  absdiflt  11860  absdifle  11861  nnabscl  11868  minclpr  12005  xrnegiso  12030  xrnegcon1d  12032  clim2  12051  climshft2  12074  sumrbdc  12148  prodrbdclem2  12342  fprodssdc  12359  sinbnd  12521  cosbnd  12522  dvdscmulr  12589  dvdsmulcr  12590  oddm1even  12644  bitsmod  12725  bitsinv1lem  12730  qredeq  12876  cncongr2  12884  isprm3  12898  prmrp  12925  sqrt2irr  12942  crth  13004  pcdvdsb  13101  ballotfilemfc0  13234  ballotfilemfcc  13235  ssnnctlemct  13339  xpsfrnel2  13669  gzsumval2  13716  imasmnd2  13761  grpid  13846  grpidrcan  13872  grpidlcan  13873  grplmulf1o  13881  imasgrp2  13915  ghmeqker  14076  abladdsub4  14120  pwselbasb  14208  imasrng  14257  imasring  14371  lspsnss2  14758  znf1o  14988  znidom  14994  znunit  14996  znrrg  14997  eltg3  15160  eltop  15172  eltop2  15173  eltop3  15174  lmbrf  15318  cncnpi  15331  txcn  15378  hmeoimaf1o  15417  ismet2  15457  xmseq0  15571  wilthlem1  16100  fsumdvdsmul  16111  lgsne0  16169  lgsquadlem1  16208  lgsquadlem2  16209  2sqlem7  16252  clwwlkn1  16671  eupth2lem2dc  16712  eupth2lem3lem3fi  16723  eupth2lem3lem6fi  16724