Theorem bitr3d 284

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  3bitrrd  309  3bitr3d  312  3bitr3rd  313  biass  388  sbcom2  2209  19.21t  2242  19.23t  2246  sbco2  2540  sbco3  2542  sbal1  2557  sbal2  2558  clelab  2904  ceqsralt  3484  csbiebt  3875  prsspwg  4783  ssprss  4784  reusv2lem5  5363  copsex2t  5461  ordtri2  6387  onmindif  6446  fnssresb  6649  fcnvres  6747  foelcdmi  6934  funcnvmpt  6983  funimass5  7042  fmptco  7118  cbvfo  7285  isocnv  7326  isoini  7334  isoselem  7337  riota2df  7388  ovmpodxf  7558  caovcanrd  7612  onmindif2  7804  ordunisuc2  7838  dfom2  7862  frxp2  8139  xpord2pred  8140  xpord3pred  8147  ordge1n0  8480  ondif2  8488  oa00  8545  odi  8565  oeoe  8586  eceqoveq  8821  isfinite2  9268  unfilem1  9275  fodomfib  9298  inficl  9395  dffi3  9401  ordiso2  9487  ordtypelem9  9498  cantnfle  9650  cantnf  9672  wemapwe  9676  rankr1a  9821  bnd2  9927  iscard  10027  domtri2  10041  nnsdomel  10042  cardaleph  10139  dfac12lem2  10194  cfss  10314  axcc3  10487  fodomb  10576  iundom2g  10595  inar1  10831  ltpiord  10943  ordpinq  10999  suplem2pr  11109  enreceq  11122  subeq0  11555  negcon1  11581  subexsub  11703  subeqrev  11707  lesub  11764  ltsub13  11766  subge0  11798  mul0or  11925  mulcan1g  11938  divmuleq  11991  mdiv  12122  ltmuldiv2  12160  lemuldiv2  12167  nn1suc  12326  addltmul  12551  elnnnn0  12618  znn0sub  12712  prime  12749  zbtwnre  13042  xadddi2  13396  supxrbnd  13427  fz1n  13643  fzrev3  13692  fzo0n  13784  fzonlt0  13785  ico01fl0  13927  divfl0  13932  modaddid  14018  modsubdir  14051  om2uzlt2i  14062  hashf1lem1  14567  wrdlenge1n0  14662  pfxccat3a  14854  sgnneg  15220  cnpart  15374  sqrt11  15396  sqrtsq2  15402  absdiflt  15452  absdifle  15453  sqreulem  15494  sqreu  15495  eqsqrtor  15501  clim2  15638  climshft2  15716  isercoll  15802  sumrb  15846  supcvg  15992  prodrblem2  16065  sinbnd  16315  cosbnd  16316  sqrt2irr  16384  dvdscmulr  16421  dvdsmulcr  16422  oddm1even  16480  bitsmod  16573  bitsinv1lem  16578  qredeq  16794  cncongr2  16805  isprm3  16820  prmrp  16850  crth  16916  pcdvdsb  17008  pceq0  17010  unbenlem  17047  ramcl  17168  pwselbasb  17620  pwsle  17625  imasleval  17674  xpsfrnel2  17697  acsfn  17794  ismon2  17870  isepi2  17877  epii  17879  fthsect  18063  fthmon  18065  isipodrs  18672  ipodrsfi  18674  imasmgm2  18824  gsumval2a  18835  imasmnd2  18929  grpid  19147  grpidrcan  19175  grpidlcan  19176  grplmulf1o  19184  grpraddf1o  19185  imasgrp2  19226  eqg0subg  19372  ghmeqker  19418  gacan  19480  odmulgeq  19732  pgpssslw  19789  efgsfo  19914  efgred  19923  abladdsub4  19986  subgdmdprd  20211  imasrng  20360  imasring  20521  0ring01eqbi  20745  domneq0r  20936  lspsnss2  21241  znf1o  21818  znfld  21827  znunit  21830  znrrg  21832  iporthcom  21902  ip2eq  21920  obsne0  21992  lindfmm  22094  lindsmm  22095  lsslinds  22098  gsumbagdiaglem  22200  psdmul  22448  matunitlindflem1  22955  matunitlindflem2  22956  matunitlindf  22957  eltg3  23241  eltop  23253  eltop2  23254  eltop3  23255  lmbrf  23539  cncnpi  23557  dfconn2  23698  1stcfb  23724  elptr  23853  xkoccn  23899  txcn  23906  hausdiag  23925  hmeoimaf1o  24050  isfbas  24109  ufileu  24199  alexsubALTlem4  24330  tsmsf1o  24425  ismet2  24613  imasdsf1olem  24653  imasf1oxmet  24655  imasf1omet  24656  xmseq0  24744  imasf1oxms  24769  metucn  24851  nrmmetd  24854  nmgt0  24910  nlmmul0or  24963  xrsxmet  25090  metdseq0  25135  elpi1i  25328  cphsqrtcl2  25468  tcphcph  25519  lmmbrf  25544  caucfil  25565  lmclim  25585  cmsss  25633  srabn  25642  ovolfioo  25749  ovolficc  25750  elovolmr  25758  ovolctb  25772  ovolicc2lem3  25801  mbfmulc2lem  25929  mbfimaopnlem  25937  itg2mulclem  26028  iblrelem  26072  ellimc2  26158  mdegle0  26356  fta1glem2  26448  dgreq0  26545  plydivlem4  26580  plydivex  26581  fta1  26592  quotcan  26595  logeftb  26874  quad2  27130  cubic2  27139  dquartlem1  27142  atandm4  27170  fsumharmonic  27302  wilthlem1  27358  basellem8  27378  mumullem2  27470  fsumdvdsmul  27485  chpchtsum  27509  logfaclbnd  27512  dchrelbas4  27533  lgsne0  27625  lgsqrlem2  27637  lgsdchrval  27644  lgsquadlem1  27670  lgsquadlem2  27671  2sqlem7  27714  addsqrexnreu  27732  dchrisum0lem1  27806  nogt01o  27986  lenlts  28042  addscan1  28313  subseq0d  28424  mulscan2d  28498  mulscan1d  28499  muls0ord  28504  ltmuldivs2wd  28521  onnolt  28585  onlts  28586  om2noseqlt2  28619  zn0subs  28722  bdaypw2n0bndlem  28782  bdayfinbndlem1  28786  trgcgrg  28911  tgcgr4  28927  tgcolg  28950  plngrotlem2  29199  lmiinv  29230  iseqlg  29345  elntg2  29496  lfuhgr  29659  cusgruvtxb  29936  upgrewlkle2  30120  clwwlkn1  30565  eupth2lem3lem3  30764  eupth2lem3lem6  30767  frgr3vlem2  30808  grpoid  31055  nvmeq0  31193  nvgt0  31209  imsmetlem  31225  nmlnogt0  31332  ip2eqi  31391  hvaddcan2  31606  hvmulcan2  31608  hvaddsub4  31613  hi2eq  31640  pjhtheu  31929  lnopeqi  32543  riesz1  32600  jpi  32805  chcv2  32891  cvp  32910  atnemeq0  32912  brabgaf  33133  fmptcof2  33184  nndiffz1  33311  nn0min  33345  xrge0addgt0  33511  rlocisunit  33770  lbslsp  33865  ressply1mon1p  34033  fldextrspunlsplem  34238  smatrcl  34361  lmlim  34512  carsggect  34884  eulerpartlems  34926  eulerpartlemgh  34944  ballotlemfc0  35059  ballotlemfcc  35060  signsvfpn  35148  signsvfnn  35149  reprdifc  35190  bnj1280  35584  fineqvnttrclselem3  35716  satffunlem1lem2  36089  elmrsubrn  36206  msubff1  36242  fz0n  36417  imageval  36614  nn0prpwlem  37032  filnetlem4  37091  onsuct0  37151  onint1  37159  dissneqlem  38183  fvineqsneu  38254  wl-sbalnae  38414  sin2h  38453  tan2h  38455  poimirlem18  38476  poimirlem21  38479  poimirlem24  38482  heicant  38493  mblfinlem3  38497  ovoliunnfl  38500  voliunnfl  38502  volsupnfl  38503  mbfresfi  38504  mbfposadd  38505  itg2addnclem  38509  itg2addnclem2  38510  itg2addnc  38512  itg2gt0cn  38513  itgaddnclem2  38517  ftc1anclem5  38535  areacirclem1  38546  areacirclem4  38549  areacirc  38551  isdmn3  38928  eldmres2  39134  cnvref4  39202  relbrcoss  39388  releldmqs  39595  lcvp  40017  lcv2  40019  lsatnem0  40022  atnem0  40295  cvlsupr2  40320  cvr2N  40388  athgt  40433  2llnmat  40501  pmap11  40739  pmapeq0  40743  2lnat  40761  paddclN  40819  pmapjat1  40830  ltrn2ateq  41157  dihcnvord  42251  dihcnv11  42252  dih0bN  42258  dih0sb  42262  dihlspsnat  42310  dihatexv2  42316  dihglblem6  42317  dochvalr  42334  dochn0nv  42352  djhcvat42  42392  dochsatshp  42428  dochshpsat  42431  dochkrsat2  42433  lcfl5a  42474  lcfl8a  42480  lclkrlem2a  42484  mapdcnvordN  42635  hdmap14lem4a  42848  hgmapeq0  42881  hdmaplkr  42890  hdmapellkr  42891  cxp111d  43321  sn-remul0ord  43387  sn-ltmulgt11d  43466  frlmfielbas  43492  eu6w  43626  rmxycomplete  43862  gicabl  44044  minregex2  44479  ntrneiel  45025  ntrneik4w  45044  ntrneik4  45045  extoimad  45108  radcnvrat  45242  pm14.123b  45354  iotavalb  45358  infxrunb3  46356  climreeq  46547  clim2f  46568  clim2f2  46602  dfodd4  48679  oddprmne2  48735  nnsgrpnmnd  49197  isidom3  49364  ovmpordxf  49373  eenglngeehlnmlem2  49772  iscnrm3  49982  uptrlem1  50240