Theorem bitr3d 280

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  3bitrrd  306  3bitr3d  309  3bitr3rd  310  biass  386  sbcom2  2161  19.21t  2199  19.23t  2203  sbco2  2515  sbco3  2517  sbal1  2533  sbal2  2534  csbiebt  3862  prsspwg  4756  ssprss  4757  reusv2lem5  5325  copsex2t  5406  copsex2gOLD  5408  ordtri2  6301  onmindif  6355  fnssresb  6554  fcnvres  6651  foelrni  6831  funimass5  6932  fmptco  7001  cbvfo  7161  isocnv  7201  isoini  7209  isoselem  7212  riota2df  7256  ovmpodxf  7423  caovcanrd  7475  onmindif2  7657  ordunisuc2  7691  dfom2  7714  ordge1n0  8324  ondif2  8332  oa00  8390  odi  8410  oeoe  8430  eceqoveq  8611  isfinite2  9072  unfilem1  9078  fodomfib  9093  inficl  9184  dffi3  9190  ordiso2  9274  ordtypelem9  9285  cantnfle  9429  cantnf  9451  wemapwe  9455  rankr1a  9594  bnd2  9651  iscard  9733  domtri2  9747  nnsdomel  9748  cardaleph  9845  dfac12lem2  9900  cfss  10021  axcc3  10194  fodomb  10282  iundom2g  10296  inar1  10531  ltpiord  10643  ordpinq  10699  suplem2pr  10809  enreceq  10822  subeq0  11247  negcon1  11273  subexsub  11393  subeqrev  11397  lesub  11454  ltsub13  11456  subge0  11488  mul0or  11615  mulcan1g  11628  div11  11661  divmuleq  11680  mdiv  11811  ltmuldiv2  11849  lemuldiv2  11856  nn1suc  11995  addltmul  12209  elnnnn0  12276  znn0sub  12367  prime  12401  zbtwnre  12686  xadddi2  13031  supxrbnd  13062  fz1n  13274  fzrev3  13322  fzo0n  13409  fzonlt0  13410  ico01fl0  13539  divfl0  13544  modsubdir  13660  om2uzlt2i  13671  hashf1lem1  14168  hashf1lem1OLD  14169  wrdlenge1n0  14253  pfxccat3a  14451  cnpart  14951  sqrt11  14974  sqrtsq2  14980  absdiflt  15029  absdifle  15030  sqreulem  15071  sqreu  15072  eqsqrtor  15078  clim2  15213  climshft2  15291  isercoll  15379  sumrb  15425  supcvg  15568  prodrblem2  15641  sinbnd  15889  cosbnd  15890  sqrt2irr  15958  dvdscmulr  15994  dvdsmulcr  15995  oddm1even  16052  bitsmod  16143  bitsinv1lem  16148  qredeq  16362  cncongr2  16373  isprm3  16388  prmrp  16417  crth  16479  pcdvdsb  16570  pceq0  16572  unbenlem  16609  ramcl  16730  pwselbasb  17199  pwsle  17203  imasleval  17252  xpsfrnel2  17275  acsfn  17368  ismon2  17446  isepi2  17453  epii  17455  fthsect  17641  fthmon  17643  isipodrs  18255  ipodrsfi  18257  gsumval2a  18369  imasmnd2  18422  grpid  18615  grpidrcan  18640  grpidlcan  18641  grplmulf1o  18649  imasgrp2  18690  ghmeqker  18861  ghmf1  18863  gacan  18911  odmulgeq  19164  pgpssslw  19219  efgsfo  19345  efgred  19354  abladdsub4  19415  subgdmdprd  19637  imasring  19858  lspsnss2  20267  0ring01eqbi  20544  znf1o  20759  znfld  20768  znunit  20771  znrrg  20773  iporthcom  20840  ip2eq  20858  obsne0  20932  lindfmm  21034  lindsmm  21035  lsslinds  21038  gsumbagdiaglemOLD  21141  gsumbagdiaglem  21144  eltg3  22112  eltop  22124  eltop2  22125  eltop3  22126  lmbrf  22411  cncnpi  22429  dfconn2  22570  1stcfb  22596  elptr  22724  xkoccn  22770  txcn  22777  hausdiag  22796  hmeoimaf1o  22921  isfbas  22980  ufileu  23070  alexsubALTlem4  23201  tsmsf1o  23296  ismet2  23486  imasdsf1olem  23526  imasf1oxmet  23528  imasf1omet  23529  xmseq0  23617  imasf1oxms  23645  metucn  23727  nrmmetd  23730  nmgt0  23786  nlmmul0or  23847  xrsxmet  23972  metdseq0  24017  elpi1i  24209  cphsqrtcl2  24350  tcphcph  24401  lmmbrf  24426  caucfil  24447  lmclim  24467  cmsss  24515  srabn  24524  ovolfioo  24631  ovolficc  24632  elovolmr  24640  ovolctb  24654  ovolicc2lem3  24683  mbfmulc2lem  24811  mbfimaopnlem  24819  itg2mulclem  24911  iblrelem  24955  ellimc2  25041  mdegle0  25242  fta1glem2  25331  dgreq0  25426  plydivlem4  25456  plydivex  25457  fta1  25468  quotcan  25469  logeftb  25739  quad2  25989  cubic2  25998  dquartlem1  26001  atandm4  26029  fsumharmonic  26161  wilthlem1  26217  basellem8  26237  mumullem2  26329  chpchtsum  26367  logfaclbnd  26370  dchrelbas4  26391  lgsne0  26483  lgsqrlem2  26495  lgsdchrval  26502  lgsquadlem1  26528  lgsquadlem2  26529  2sqlem7  26572  addsqrexnreu  26590  dchrisum0lem1  26664  trgcgrg  26876  tgcgr4  26892  tgcolg  26915  lmiinv  27153  iseqlg  27228  elntg2  27353  cusgruvtxb  27789  upgrewlkle2  27973  clwwlkn1  28405  eupth2lem3lem3  28594  eupth2lem3lem6  28597  frgr3vlem2  28638  grpoid  28882  nvmeq0  29020  nvgt0  29036  imsmetlem  29052  nmlnogt0  29159  ip2eqi  29218  hvaddcan2  29433  hvmulcan2  29435  hvaddsub4  29440  hi2eq  29467  pjhtheu  29756  lnopeqi  30370  riesz1  30427  jpi  30632  chcv2  30718  cvp  30737  atnemeq0  30739  brabgaf  30948  fmptcof2  30994  funcnvmpt  31004  nndiffz1  31107  nn0min  31134  xrge0addgt0  31300  lbslsp  31572  smatrcl  31746  lmlim  31897  carsggect  32285  eulerpartlems  32327  eulerpartlemgh  32345  ballotlemfc0  32459  ballotlemfcc  32460  sgnneg  32507  signsvfpn  32564  signsvfnn  32565  reprdifc  32607  bnj1280  33000  lfuhgr  33079  satffunlem1lem2  33365  elmrsubrn  33482  msubff1  33518  fz0n  33696  frxp2  33791  xpord2pred  33792  nogt01o  33899  slenlt  33955  imageval  34232  nn0prpwlem  34511  filnetlem4  34570  onsuct0  34630  onint1  34638  dissneqlem  35511  fvineqsneu  35582  wl-sbalnae  35717  wl-ax11-lem8  35743  wl-ax11-lem10  35745  sin2h  35767  tan2h  35769  matunitlindflem1  35773  matunitlindflem2  35774  matunitlindf  35775  poimirlem18  35795  poimirlem21  35798  poimirlem24  35801  heicant  35812  mblfinlem3  35816  ovoliunnfl  35819  voliunnfl  35821  volsupnfl  35822  mbfresfi  35823  mbfposadd  35824  itg2addnclem  35828  itg2addnclem2  35829  itg2addnc  35831  itg2gt0cn  35832  itgaddnclem2  35836  ftc1anclem5  35854  areacirclem1  35865  areacirclem4  35868  areacirc  35870  isdmn3  36232  eldmres2  36410  relbrcoss  36564  releldmqs  36770  lcvp  37054  lcv2  37056  lsatnem0  37059  atnem0  37332  cvlsupr2  37357  cvr2N  37425  athgt  37470  2llnmat  37538  pmap11  37776  pmapeq0  37780  2lnat  37798  paddclN  37856  pmapjat1  37867  ltrn2ateq  38194  dihcnvord  39288  dihcnv11  39289  dih0bN  39295  dih0sb  39299  dihlspsnat  39347  dihatexv2  39353  dihglblem6  39354  dochvalr  39371  dochn0nv  39389  djhcvat42  39429  dochsatshp  39465  dochshpsat  39468  dochkrsat2  39470  lcfl5a  39511  lcfl8a  39517  lclkrlem2a  39521  mapdcnvordN  39672  hdmap14lem4a  39885  hgmapeq0  39918  hdmaplkr  39927  hdmapellkr  39928  metakunt15  40139  frlmfielbas  40231  rmxycomplete  40739  gicabl  40924  minregex2  41142  ntrneiel  41691  ntrneik4w  41710  ntrneik4  41711  extoimad  41775  radcnvrat  41932  pm14.123b  42044  iotavalb  42048  infxrunb3  42964  climreeq  43154  clim2f  43177  clim2f2  43211  dfodd4  45111  oddprmne2  45167  nnsgrpnmnd  45372  ovmpordxf  45674  eenglngeehlnmlem2  46084  iscnrm3  46246