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  2179  19.21t  2214  19.23t  2218  sbco2  2516  sbco3  2518  sbal1  2533  sbal2  2534  clelab  2881  ceqsralt  3465  csbiebt  3867  prsspwg  4767  ssprss  4768  reusv2lem5  5345  copsex2t  5447  ordtri2  6359  onmindif  6418  fnssresb  6621  fcnvres  6718  foelcdmi  6902  funcnvmpt  6950  funimass5  7008  fmptco  7083  cbvfo  7244  isocnv  7285  isoini  7293  isoselem  7296  riota2df  7347  ovmpodxf  7517  caovcanrd  7570  onmindif2  7761  ordunisuc2  7795  dfom2  7819  frxp2  8094  xpord2pred  8095  xpord3pred  8102  ordge1n0  8429  ondif2  8437  oa00  8494  odi  8514  oeoe  8535  eceqoveq  8769  isfinite2  9208  unfilem1  9215  fodomfib  9239  fodomfibOLD  9241  inficl  9338  dffi3  9344  ordiso2  9430  ordtypelem9  9441  cantnfle  9592  cantnf  9614  wemapwe  9618  rankr1a  9760  bnd2  9817  iscard  9899  domtri2  9913  nnsdomel  9914  cardaleph  10011  dfac12lem2  10067  cfss  10187  axcc3  10360  fodomb  10448  iundom2g  10462  inar1  10698  ltpiord  10810  ordpinq  10866  suplem2pr  10976  enreceq  10989  subeq0  11420  negcon1  11446  subexsub  11568  subeqrev  11572  lesub  11629  ltsub13  11631  subge0  11663  mul0or  11790  mulcan1g  11803  div11OLD  11838  divmuleq  11860  mdiv  11991  ltmuldiv2  12030  lemuldiv2  12037  nn1suc  12196  addltmul  12413  elnnnn0  12480  znn0sub  12574  prime  12610  zbtwnre  12896  xadddi2  13249  supxrbnd  13280  fz1n  13496  fzrev3  13544  fzo0n  13636  fzonlt0  13637  ico01fl0  13778  divfl0  13783  modaddid  13869  modsubdir  13902  om2uzlt2i  13913  hashf1lem1  14417  wrdlenge1n0  14512  pfxccat3a  14700  cnpart  15202  sqrt11  15224  sqrtsq2  15230  absdiflt  15280  absdifle  15281  sqreulem  15322  sqreu  15323  eqsqrtor  15329  clim2  15466  climshft2  15544  isercoll  15630  sumrb  15675  supcvg  15821  prodrblem2  15896  sinbnd  16147  cosbnd  16148  sqrt2irr  16216  dvdscmulr  16253  dvdsmulcr  16254  oddm1even  16312  bitsmod  16405  bitsinv1lem  16410  qredeq  16626  cncongr2  16637  isprm3  16652  prmrp  16682  crth  16748  pcdvdsb  16840  pceq0  16842  unbenlem  16879  ramcl  17000  pwselbasb  17451  pwsle  17456  imasleval  17505  xpsfrnel2  17528  acsfn  17625  ismon2  17701  isepi2  17708  epii  17710  fthsect  17894  fthmon  17896  isipodrs  18503  ipodrsfi  18505  gsumval2a  18653  imasmnd2  18742  grpid  18951  grpidrcan  18979  grpidlcan  18980  grplmulf1o  18989  grpraddf1o  18990  imasgrp2  19031  eqg0subg  19171  ghmeqker  19218  gacan  19280  odmulgeq  19532  pgpssslw  19589  efgsfo  19714  efgred  19723  abladdsub4  19786  subgdmdprd  20011  imasrng  20158  imasring  20310  0ring01eqbi  20509  domneq0r  20701  lspsnss2  21000  znf1o  21531  znfld  21540  znunit  21543  znrrg  21545  iporthcom  21615  ip2eq  21633  obsne0  21705  lindfmm  21807  lindsmm  21808  lsslinds  21811  gsumbagdiaglem  21910  psdmul  22132  eltg3  22927  eltop  22939  eltop2  22940  eltop3  22941  lmbrf  23225  cncnpi  23243  dfconn2  23384  1stcfb  23410  elptr  23538  xkoccn  23584  txcn  23591  hausdiag  23610  hmeoimaf1o  23735  isfbas  23794  ufileu  23884  alexsubALTlem4  24015  tsmsf1o  24110  ismet2  24298  imasdsf1olem  24338  imasf1oxmet  24340  imasf1omet  24341  xmseq0  24429  imasf1oxms  24454  metucn  24536  nrmmetd  24539  nmgt0  24595  nlmmul0or  24648  xrsxmet  24775  metdseq0  24820  elpi1i  25013  cphsqrtcl2  25153  tcphcph  25204  lmmbrf  25229  caucfil  25250  lmclim  25270  cmsss  25318  srabn  25327  ovolfioo  25434  ovolficc  25435  elovolmr  25443  ovolctb  25457  ovolicc2lem3  25486  mbfmulc2lem  25614  mbfimaopnlem  25622  itg2mulclem  25713  iblrelem  25758  ellimc2  25844  mdegle0  26042  fta1glem2  26134  dgreq0  26230  plydivlem4  26262  plydivex  26263  fta1  26274  quotcan  26275  logeftb  26547  quad2  26803  cubic2  26812  dquartlem1  26815  atandm4  26843  fsumharmonic  26975  wilthlem1  27031  basellem8  27051  mumullem2  27143  fsumdvdsmul  27158  chpchtsum  27182  logfaclbnd  27185  dchrelbas4  27206  lgsne0  27298  lgsqrlem2  27310  lgsdchrval  27317  lgsquadlem1  27343  lgsquadlem2  27344  2sqlem7  27387  addsqrexnreu  27405  dchrisum0lem1  27479  nogt01o  27660  lenlts  27716  addscan1  27986  subseq0d  28097  mulscan2d  28171  mulscan1d  28172  muls0ord  28177  ltmuldivs2wd  28194  onnolt  28258  onlts  28259  om2noseqlt2  28292  zn0subs  28395  bdaypw2n0bndlem  28455  bdayfinbndlem1  28459  trgcgrg  28583  tgcgr4  28599  tgcolg  28622  lmiinv  28860  iseqlg  28935  elntg2  29054  cusgruvtxb  29491  upgrewlkle2  29675  clwwlkn1  30111  eupth2lem3lem3  30300  eupth2lem3lem6  30303  frgr3vlem2  30344  grpoid  30591  nvmeq0  30729  nvgt0  30745  imsmetlem  30761  nmlnogt0  30868  ip2eqi  30927  hvaddcan2  31142  hvmulcan2  31144  hvaddsub4  31149  hi2eq  31176  pjhtheu  31465  lnopeqi  32079  riesz1  32136  jpi  32341  chcv2  32427  cvp  32446  atnemeq0  32448  brabgaf  32679  fmptcof2  32730  nndiffz1  32859  nn0min  32894  sgnneg  32906  xrge0addgt0  33077  lbslsp  33437  ressply1mon1p  33628  fldextrspunlsplem  33817  smatrcl  33940  lmlim  34091  carsggect  34462  eulerpartlems  34504  eulerpartlemgh  34522  ballotlemfc0  34637  ballotlemfcc  34638  signsvfpn  34729  signsvfnn  34730  reprdifc  34771  bnj1280  35162  fineqvnttrclselem3  35267  lfuhgr  35300  satffunlem1lem2  35585  elmrsubrn  35702  msubff1  35738  fz0n  35913  imageval  36110  nn0prpwlem  36504  filnetlem4  36563  onsuct0  36623  onint1  36631  dissneqlem  37656  fvineqsneu  37727  wl-sbalnae  37887  sin2h  37931  tan2h  37933  matunitlindflem1  37937  matunitlindflem2  37938  matunitlindf  37939  poimirlem18  37959  poimirlem21  37962  poimirlem24  37965  heicant  37976  mblfinlem3  37980  ovoliunnfl  37983  voliunnfl  37985  volsupnfl  37986  mbfresfi  37987  mbfposadd  37988  itg2addnclem  37992  itg2addnclem2  37993  itg2addnc  37995  itg2gt0cn  37996  itgaddnclem2  38000  ftc1anclem5  38018  areacirclem1  38029  areacirclem4  38032  areacirc  38034  isdmn3  38395  eldmres2  38603  cnvref4  38671  relbrcoss  38857  releldmqs  39064  lcvp  39486  lcv2  39488  lsatnem0  39491  atnem0  39764  cvlsupr2  39789  cvr2N  39857  athgt  39902  2llnmat  39970  pmap11  40208  pmapeq0  40212  2lnat  40230  paddclN  40288  pmapjat1  40299  ltrn2ateq  40626  dihcnvord  41720  dihcnv11  41721  dih0bN  41727  dih0sb  41731  dihlspsnat  41779  dihatexv2  41785  dihglblem6  41786  dochvalr  41803  dochn0nv  41821  djhcvat42  41861  dochsatshp  41897  dochshpsat  41900  dochkrsat2  41902  lcfl5a  41943  lcfl8a  41949  lclkrlem2a  41953  mapdcnvordN  42104  hdmap14lem4a  42317  hgmapeq0  42350  hdmaplkr  42359  hdmapellkr  42360  cxp111d  42774  sn-remul0ord  42840  sn-ltmulgt11d  42919  frlmfielbas  42945  eu6w  43109  rmxycomplete  43345  gicabl  43527  minregex2  43962  ntrneiel  44508  ntrneik4w  44527  ntrneik4  44528  extoimad  44591  radcnvrat  44741  pm14.123b  44853  iotavalb  44857  infxrunb3  45852  climreeq  46043  clim2f  46064  clim2f2  46098  dfodd4  48129  oddprmne2  48185  nnsgrpnmnd  48648  ovmpordxf  48809  eenglngeehlnmlem2  49208  iscnrm3  49421  uptrlem1  49679