Theorem bitr3d 281

Description: Deduction form of bitr3i 277. (Contributed by NM, 14-May-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 223	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜓))
3		bitr3d.2	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4	2, 3	bitrd 279	1 ⊢ (𝜑 → (𝜒 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  3bitrrd  306  3bitr3d  309  3bitr3rd  310  biass  384  sbcom2  2178  19.21t  2213  19.23t  2217  sbco2  2514  sbco3  2516  sbal1  2531  sbal2  2532  clelab  2879  ceqsralt  3462  csbiebt  3862  prsspwg  4756  ssprss  4757  reusv2lem5  5333  copsex2t  5435  ordtri2  6347  onmindif  6406  fnssresb  6609  fcnvres  6706  foelcdmi  6890  funcnvmpt  6938  funimass5  6996  fmptco  7071  cbvfo  7233  isocnv  7274  isoini  7282  isoselem  7285  riota2df  7336  ovmpodxf  7506  caovcanrd  7559  onmindif2  7750  ordunisuc2  7784  dfom2  7808  frxp2  8083  xpord2pred  8084  xpord3pred  8091  ordge1n0  8418  ondif2  8426  oa00  8483  odi  8503  oeoe  8524  eceqoveq  8758  isfinite2  9197  unfilem1  9204  fodomfib  9228  fodomfibOLD  9230  inficl  9327  dffi3  9333  ordiso2  9419  ordtypelem9  9430  cantnfle  9581  cantnf  9603  wemapwe  9607  rankr1a  9749  bnd2  9806  iscard  9888  domtri2  9902  nnsdomel  9903  cardaleph  10000  dfac12lem2  10056  cfss  10176  axcc3  10349  fodomb  10437  iundom2g  10451  inar1  10687  ltpiord  10799  ordpinq  10855  suplem2pr  10965  enreceq  10978  subeq0  11409  negcon1  11435  subexsub  11557  subeqrev  11561  lesub  11618  ltsub13  11620  subge0  11652  mul0or  11779  mulcan1g  11792  div11OLD  11827  divmuleq  11849  mdiv  11980  ltmuldiv2  12019  lemuldiv2  12026  nn1suc  12185  addltmul  12402  elnnnn0  12469  znn0sub  12563  prime  12599  zbtwnre  12885  xadddi2  13238  supxrbnd  13269  fz1n  13485  fzrev3  13533  fzo0n  13625  fzonlt0  13626  ico01fl0  13767  divfl0  13772  modaddid  13858  modsubdir  13891  om2uzlt2i  13902  hashf1lem1  14406  wrdlenge1n0  14501  pfxccat3a  14689  cnpart  15191  sqrt11  15213  sqrtsq2  15219  absdiflt  15269  absdifle  15270  sqreulem  15311  sqreu  15312  eqsqrtor  15318  clim2  15455  climshft2  15533  isercoll  15619  sumrb  15664  supcvg  15810  prodrblem2  15885  sinbnd  16136  cosbnd  16137  sqrt2irr  16205  dvdscmulr  16242  dvdsmulcr  16243  oddm1even  16301  bitsmod  16394  bitsinv1lem  16399  qredeq  16615  cncongr2  16626  isprm3  16641  prmrp  16671  crth  16737  pcdvdsb  16829  pceq0  16831  unbenlem  16868  ramcl  16989  pwselbasb  17440  pwsle  17445  imasleval  17494  xpsfrnel2  17517  acsfn  17614  ismon2  17690  isepi2  17697  epii  17699  fthsect  17883  fthmon  17885  isipodrs  18492  ipodrsfi  18494  gsumval2a  18642  imasmnd2  18731  grpid  18940  grpidrcan  18968  grpidlcan  18969  grplmulf1o  18978  grpraddf1o  18979  imasgrp2  19020  eqg0subg  19160  ghmeqker  19207  gacan  19269  odmulgeq  19521  pgpssslw  19578  efgsfo  19703  efgred  19712  abladdsub4  19775  subgdmdprd  20000  imasrng  20147  imasring  20299  0ring01eqbi  20498  domneq0r  20690  lspsnss2  20989  znf1o  21520  znfld  21529  znunit  21532  znrrg  21534  iporthcom  21604  ip2eq  21622  obsne0  21694  lindfmm  21796  lindsmm  21797  lsslinds  21800  gsumbagdiaglem  21899  psdmul  22121  eltg3  22915  eltop  22927  eltop2  22928  eltop3  22929  lmbrf  23213  cncnpi  23231  dfconn2  23372  1stcfb  23398  elptr  23526  xkoccn  23572  txcn  23579  hausdiag  23598  hmeoimaf1o  23723  isfbas  23782  ufileu  23872  alexsubALTlem4  24003  tsmsf1o  24098  ismet2  24286  imasdsf1olem  24326  imasf1oxmet  24328  imasf1omet  24329  xmseq0  24417  imasf1oxms  24442  metucn  24524  nrmmetd  24527  nmgt0  24583  nlmmul0or  24636  xrsxmet  24763  metdseq0  24808  elpi1i  25001  cphsqrtcl2  25141  tcphcph  25192  lmmbrf  25217  caucfil  25238  lmclim  25258  cmsss  25306  srabn  25315  ovolfioo  25422  ovolficc  25423  elovolmr  25431  ovolctb  25445  ovolicc2lem3  25474  mbfmulc2lem  25602  mbfimaopnlem  25610  itg2mulclem  25701  iblrelem  25746  ellimc2  25832  mdegle0  26030  fta1glem2  26122  dgreq0  26218  plydivlem4  26250  plydivex  26251  fta1  26262  quotcan  26263  logeftb  26535  quad2  26791  cubic2  26800  dquartlem1  26803  atandm4  26831  fsumharmonic  26963  wilthlem1  27019  basellem8  27039  mumullem2  27131  fsumdvdsmul  27146  chpchtsum  27170  logfaclbnd  27173  dchrelbas4  27194  lgsne0  27286  lgsqrlem2  27298  lgsdchrval  27305  lgsquadlem1  27331  lgsquadlem2  27332  2sqlem7  27375  addsqrexnreu  27393  dchrisum0lem1  27467  nogt01o  27648  lenlts  27704  addscan1  27974  subseq0d  28085  mulscan2d  28159  mulscan1d  28160  muls0ord  28165  ltmuldivs2wd  28182  onnolt  28246  onlts  28247  om2noseqlt2  28280  zn0subs  28383  bdaypw2n0bndlem  28443  bdayfinbndlem1  28447  trgcgrg  28571  tgcgr4  28587  tgcolg  28610  lmiinv  28848  iseqlg  28923  elntg2  29042  cusgruvtxb  29479  upgrewlkle2  29663  clwwlkn1  30099  eupth2lem3lem3  30288  eupth2lem3lem6  30291  frgr3vlem2  30332  grpoid  30579  nvmeq0  30717  nvgt0  30733  imsmetlem  30749  nmlnogt0  30856  ip2eqi  30915  hvaddcan2  31130  hvmulcan2  31132  hvaddsub4  31137  hi2eq  31164  pjhtheu  31453  lnopeqi  32067  riesz1  32124  jpi  32329  chcv2  32415  cvp  32434  atnemeq0  32436  brabgaf  32667  fmptcof2  32718  nndiffz1  32847  nn0min  32882  sgnneg  32894  xrge0addgt0  33065  lbslsp  33425  ressply1mon1p  33616  fldextrspunlsplem  33805  smatrcl  33928  lmlim  34079  carsggect  34450  eulerpartlems  34492  eulerpartlemgh  34510  ballotlemfc0  34625  ballotlemfcc  34626  signsvfpn  34717  signsvfnn  34718  reprdifc  34759  bnj1280  35150  fineqvnttrclselem3  35255  lfuhgr  35288  satffunlem1lem2  35573  elmrsubrn  35690  msubff1  35726  fz0n  35901  imageval  36098  nn0prpwlem  36492  filnetlem4  36551  onsuct0  36611  onint1  36619  dissneqlem  37644  fvineqsneu  37715  wl-sbalnae  37875  sin2h  37919  tan2h  37921  matunitlindflem1  37925  matunitlindflem2  37926  matunitlindf  37927  poimirlem18  37947  poimirlem21  37950  poimirlem24  37953  heicant  37964  mblfinlem3  37968  ovoliunnfl  37971  voliunnfl  37973  volsupnfl  37974  mbfresfi  37975  mbfposadd  37976  itg2addnclem  37980  itg2addnclem2  37981  itg2addnc  37983  itg2gt0cn  37984  itgaddnclem2  37988  ftc1anclem5  38006  areacirclem1  38017  areacirclem4  38020  areacirc  38022  isdmn3  38383  eldmres2  38591  cnvref4  38659  relbrcoss  38845  releldmqs  39052  lcvp  39474  lcv2  39476  lsatnem0  39479  atnem0  39752  cvlsupr2  39777  cvr2N  39845  athgt  39890  2llnmat  39958  pmap11  40196  pmapeq0  40200  2lnat  40218  paddclN  40276  pmapjat1  40287  ltrn2ateq  40614  dihcnvord  41708  dihcnv11  41709  dih0bN  41715  dih0sb  41719  dihlspsnat  41767  dihatexv2  41773  dihglblem6  41774  dochvalr  41791  dochn0nv  41809  djhcvat42  41849  dochsatshp  41885  dochshpsat  41888  dochkrsat2  41890  lcfl5a  41931  lcfl8a  41937  lclkrlem2a  41941  mapdcnvordN  42092  hdmap14lem4a  42305  hgmapeq0  42338  hdmaplkr  42347  hdmapellkr  42348  cxp111d  42762  sn-remul0ord  42828  sn-ltmulgt11d  42907  frlmfielbas  42933  eu6w  43097  rmxycomplete  43333  gicabl  43515  minregex2  43950  ntrneiel  44496  ntrneik4w  44515  ntrneik4  44516  extoimad  44579  radcnvrat  44729  pm14.123b  44841  iotavalb  44845  infxrunb3  45840  climreeq  46031  clim2f  46052  clim2f2  46086  dfodd4  48123  oddprmne2  48179  nnsgrpnmnd  48642  ovmpordxf  48803  eenglngeehlnmlem2  49202  iscnrm3  49415  uptrlem1  49673