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  2206  19.21t  2241  19.23t  2245  sbco2  2542  sbco3  2544  sbal1  2559  sbal2  2560  clelab  2906  ceqsralt  3488  csbiebt  3881  prsspwg  4788  ssprss  4789  reusv2lem5  5372  copsex2t  5474  ordtri2  6396  onmindif  6455  fnssresb  6657  fcnvres  6755  foelcdmi  6942  funcnvmpt  6991  funimass5  7050  fmptco  7125  cbvfo  7287  isocnv  7328  isoini  7336  isoselem  7339  riota2df  7392  ovmpodxf  7562  caovcanrd  7615  onmindif2  7804  ordunisuc2  7838  dfom2  7862  frxp2  8138  xpord2pred  8139  xpord3pred  8146  ordge1n0  8477  ondif2  8485  oa00  8542  odi  8562  oeoe  8583  eceqoveq  8818  isfinite2  9256  unfilem1  9263  fodomfib  9286  inficl  9383  dffi3  9389  ordiso2  9475  ordtypelem9  9486  cantnfle  9638  cantnf  9660  wemapwe  9664  rankr1a  9806  bnd2  9883  iscard  9968  domtri2  9982  nnsdomel  9983  cardaleph  10080  dfac12lem2  10135  cfss  10255  axcc3  10428  fodomb  10516  iundom2g  10530  inar1  10766  ltpiord  10878  ordpinq  10934  suplem2pr  11044  enreceq  11057  subeq0  11490  negcon1  11516  subexsub  11638  subeqrev  11642  lesub  11699  ltsub13  11701  subge0  11733  mul0or  11860  mulcan1g  11873  divmuleq  11926  mdiv  12057  ltmuldiv2  12095  lemuldiv2  12102  nn1suc  12261  addltmul  12486  elnnnn0  12553  znn0sub  12647  prime  12683  zbtwnre  12976  xadddi2  13329  supxrbnd  13360  fz1n  13576  fzrev3  13625  fzo0n  13717  fzonlt0  13718  ico01fl0  13859  divfl0  13864  modaddid  13950  modsubdir  13983  om2uzlt2i  13994  hashf1lem1  14499  wrdlenge1n0  14594  pfxccat3a  14782  sgnneg  15144  cnpart  15298  sqrt11  15320  sqrtsq2  15326  absdiflt  15376  absdifle  15377  sqreulem  15418  sqreu  15419  eqsqrtor  15425  clim2  15562  climshft2  15640  isercoll  15726  sumrb  15771  supcvg  15917  prodrblem2  15992  sinbnd  16242  cosbnd  16243  sqrt2irr  16311  dvdscmulr  16348  dvdsmulcr  16349  oddm1even  16407  bitsmod  16500  bitsinv1lem  16505  qredeq  16721  cncongr2  16732  isprm3  16747  prmrp  16777  crth  16843  pcdvdsb  16935  pceq0  16937  unbenlem  16974  ramcl  17095  pwselbasb  17547  pwsle  17552  imasleval  17601  xpsfrnel2  17624  acsfn  17721  ismon2  17797  isepi2  17804  epii  17806  fthsect  17990  fthmon  17992  isipodrs  18599  ipodrsfi  18601  gsumval2a  18749  imasmnd2  18838  grpid  19048  grpidrcan  19076  grpidlcan  19077  grplmulf1o  19085  grpraddf1o  19086  imasgrp2  19127  eqg0subg  19273  ghmeqker  19319  gacan  19381  odmulgeq  19633  pgpssslw  19690  efgsfo  19815  efgred  19824  abladdsub4  19887  subgdmdprd  20112  imasrng  20261  imasring  20419  0ring01eqbi  20642  domneq0r  20833  lspsnss2  21137  znf1o  21712  znfld  21721  znunit  21724  znrrg  21726  iporthcom  21796  ip2eq  21814  obsne0  21886  lindfmm  21988  lindsmm  21989  lsslinds  21992  gsumbagdiaglem  22092  psdmul  22340  eltg3  23130  eltop  23142  eltop2  23143  eltop3  23144  lmbrf  23428  cncnpi  23446  dfconn2  23587  1stcfb  23613  elptr  23741  xkoccn  23787  txcn  23794  hausdiag  23813  hmeoimaf1o  23938  isfbas  23997  ufileu  24087  alexsubALTlem4  24218  tsmsf1o  24313  ismet2  24501  imasdsf1olem  24541  imasf1oxmet  24543  imasf1omet  24544  xmseq0  24632  imasf1oxms  24657  metucn  24739  nrmmetd  24742  nmgt0  24798  nlmmul0or  24851  xrsxmet  24978  metdseq0  25023  elpi1i  25216  cphsqrtcl2  25356  tcphcph  25407  lmmbrf  25432  caucfil  25453  lmclim  25473  cmsss  25521  srabn  25530  ovolfioo  25637  ovolficc  25638  elovolmr  25646  ovolctb  25660  ovolicc2lem3  25689  mbfmulc2lem  25817  mbfimaopnlem  25825  itg2mulclem  25916  iblrelem  25961  ellimc2  26047  mdegle0  26245  fta1glem2  26337  dgreq0  26433  plydivlem4  26468  plydivex  26469  fta1  26480  quotcan  26481  logeftb  26759  quad2  27015  cubic2  27024  dquartlem1  27027  atandm4  27055  fsumharmonic  27187  wilthlem1  27243  basellem8  27263  mumullem2  27355  fsumdvdsmul  27370  chpchtsum  27394  logfaclbnd  27397  dchrelbas4  27418  lgsne0  27510  lgsqrlem2  27522  lgsdchrval  27529  lgsquadlem1  27555  lgsquadlem2  27556  2sqlem7  27599  addsqrexnreu  27617  dchrisum0lem1  27691  nogt01o  27871  lenlts  27927  addscan1  28198  subseq0d  28309  mulscan2d  28383  mulscan1d  28384  muls0ord  28389  ltmuldivs2wd  28406  onnolt  28470  onlts  28471  om2noseqlt2  28504  zn0subs  28607  bdaypw2n0bndlem  28667  bdayfinbndlem1  28671  trgcgrg  28795  tgcgr4  28811  tgcolg  28834  plngrotlem2  29081  lmiinv  29112  iseqlg  29195  elntg2  29346  cusgruvtxb  29783  upgrewlkle2  29967  clwwlkn1  30403  eupth2lem3lem3  30592  eupth2lem3lem6  30595  frgr3vlem2  30636  grpoid  30883  nvmeq0  31021  nvgt0  31037  imsmetlem  31053  nmlnogt0  31160  ip2eqi  31219  hvaddcan2  31434  hvmulcan2  31436  hvaddsub4  31441  hi2eq  31468  pjhtheu  31757  lnopeqi  32371  riesz1  32428  jpi  32633  chcv2  32719  cvp  32738  atnemeq0  32740  brabgaf  32962  fmptcof2  33013  nndiffz1  33142  nn0min  33176  xrge0addgt0  33346  rlocisunit  33605  lbslsp  33699  ressply1mon1p  33867  fldextrspunlsplem  34072  smatrcl  34195  lmlim  34346  carsggect  34717  eulerpartlems  34759  eulerpartlemgh  34777  ballotlemfc0  34892  ballotlemfcc  34893  signsvfpn  34981  signsvfnn  34982  reprdifc  35023  bnj1280  35417  fineqvnttrclselem3  35544  lfuhgr  35618  satffunlem1lem2  35903  elmrsubrn  36020  msubff1  36056  fz0n  36231  imageval  36428  nn0prpwlem  36861  filnetlem4  36920  onsuct0  36980  onint1  36988  dissneqlem  38014  fvineqsneu  38085  wl-sbalnae  38245  sin2h  38289  tan2h  38291  matunitlindflem1  38295  matunitlindflem2  38296  matunitlindf  38297  poimirlem18  38317  poimirlem21  38320  poimirlem24  38323  heicant  38334  mblfinlem3  38338  ovoliunnfl  38341  voliunnfl  38343  volsupnfl  38344  mbfresfi  38345  mbfposadd  38346  itg2addnclem  38350  itg2addnclem2  38351  itg2addnc  38353  itg2gt0cn  38354  itgaddnclem2  38358  ftc1anclem5  38376  areacirclem1  38387  areacirclem4  38390  areacirc  38392  isdmn3  38753  eldmres2  38959  cnvref4  39027  relbrcoss  39213  releldmqs  39420  lcvp  39842  lcv2  39844  lsatnem0  39847  atnem0  40120  cvlsupr2  40145  cvr2N  40213  athgt  40258  2llnmat  40326  pmap11  40564  pmapeq0  40568  2lnat  40586  paddclN  40644  pmapjat1  40655  ltrn2ateq  40982  dihcnvord  42076  dihcnv11  42077  dih0bN  42083  dih0sb  42087  dihlspsnat  42135  dihatexv2  42141  dihglblem6  42142  dochvalr  42159  dochn0nv  42177  djhcvat42  42217  dochsatshp  42253  dochshpsat  42256  dochkrsat2  42258  lcfl5a  42299  lcfl8a  42305  lclkrlem2a  42309  mapdcnvordN  42460  hdmap14lem4a  42673  hgmapeq0  42706  hdmaplkr  42715  hdmapellkr  42716  cxp111d  43131  sn-remul0ord  43197  sn-ltmulgt11d  43276  frlmfielbas  43302  eu6w  43436  rmxycomplete  43672  gicabl  43854  minregex2  44289  ntrneiel  44835  ntrneik4w  44854  ntrneik4  44855  extoimad  44918  radcnvrat  45052  pm14.123b  45164  iotavalb  45168  infxrunb3  46166  climreeq  46357  clim2f  46378  clim2f2  46412  dfodd4  48452  oddprmne2  48508  nnsgrpnmnd  48971  isidom3  49138  ovmpordxf  49147  eenglngeehlnmlem2  49546  iscnrm3  49758  uptrlem1  50016