Theorem bitr3d 269

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

Syntax hints:   → wi 4   ↔ wb 195

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 196

This theorem is referenced by:  3bitrrd  294  3bitr3d  297  3bitr3rd  298  biass  373  sbco2  2403  sbco3  2405  sbcom2  2433  sbal1  2448  sbal2  2449  sbal  2450  csbiebt  3519  prsspwg  4295  ssprss  4296  reusv2lem5  4799  copsex2t  4883  copsex2g  4884  ordtri2  5675  onmindif  5732  fnssresb  5917  fcnvres  5995  foelrni  6154  funimass5  6242  fmptco  6303  cbvfo  6444  isocnv  6480  isoini  6488  isoselem  6491  riota2df  6531  ovmpt2dxf  6684  caovcanrd  6735  onmindif2  6904  ordunisuc2  6936  dfom2  6959  ordge1n0  7465  ondif2  7469  oa00  7526  odi  7546  oeoe  7566  eceqoveq  7740  isfinite2  8103  unfilem1  8109  fodomfib  8125  inficl  8214  dffi3  8220  ordiso2  8303  ordtypelem9  8314  cantnfle  8451  cantnf  8473  wemapwe  8477  rankr1a  8582  bnd2  8639  iscard  8684  domtri2  8698  nnsdomel  8699  cardaleph  8795  dfac12lem2  8849  cfss  8970  axcc3  9143  fodomb  9229  iundom2g  9241  inar1  9476  ltpiord  9588  ordpinq  9644  suplem2pr  9754  enreceq  9766  subeq0  10186  negcon1  10212  subexsub  10328  subeqrev  10332  lesub  10386  ltsub13  10388  subge0  10420  mul0or  10546  mulcan1g  10559  div11  10592  divmuleq  10609  ltmuldiv2  10776  lemuldiv2  10783  nn1suc  10918  addltmul  11145  elnnnn0  11213  znn0sub  11301  prime  11334  zbtwnre  11662  xadddi2  11999  supxrbnd  12030  fz1n  12230  fzrev3  12276  fzo0n  12359  fzonlt0  12360  ico01fl0  12482  modsubdir  12601  om2uzlt2i  12612  hashf1lem1  13096  wrdlenge1n0  13195  cnpart  13828  sqrt11  13851  sqrtsq2  13857  absdiflt  13905  absdifle  13906  sqreulem  13947  sqreu  13948  eqsqrtor  13954  clim2  14083  climshft2  14161  isercoll  14246  sumrb  14291  supcvg  14427  prodrblem2  14500  sinbnd  14749  cosbnd  14750  sqrt2irr  14817  dvdscmulr  14848  dvdsmulcr  14849  oddm1even  14905  bitsmod  14996  bitsinv1lem  15001  qredeq  15209  cncongr2  15220  isprm3  15234  prmrp  15262  crth  15321  pcdvdsb  15411  pceq0  15413  unbenlem  15450  ramcl  15571  pwselbasb  15971  pwsle  15975  imasleval  16024  xpsfrnel2  16048  acsfn  16143  ismon2  16217  isepi2  16224  epii  16226  fthsect  16408  fthmon  16410  isipodrs  16984  ipodrsfi  16986  gsumval2a  17102  imasmnd2  17150  grpid  17280  grpidrcan  17303  grpidlcan  17304  grplmulf1o  17312  imasgrp2  17353  ghmeqker  17510  ghmf1  17512  gacan  17561  odmulgeq  17797  pgpssslw  17852  efgsfo  17975  efgred  17984  abladdsub4  18042  subgdmdprd  18256  imasring  18442  lspsnss2  18826  0ring01eqbi  19094  gsumbagdiaglem  19196  znf1o  19719  znfld  19728  znunit  19731  znrrg  19733  iporthcom  19799  ip2eq  19817  obsne0  19888  lindfmm  19985  lindsmm  19986  lsslinds  19989  eltg3  20577  eltop  20589  eltop2  20590  eltop3  20591  lmbrf  20874  cncnpi  20892  dfcon2  21032  1stcfb  21058  elptr  21186  xkoccn  21232  txcn  21239  hausdiag  21258  hmeoimaf1o  21383  isfbas  21443  ufileu  21533  alexsubALTlem4  21664  tsmsf1o  21758  ismet2  21948  imasdsf1olem  21988  imasf1oxmet  21990  imasf1omet  21991  xmseq0  22079  imasf1oxms  22104  metucn  22186  nrmmetd  22189  nmgt0  22244  nlmmul0or  22297  xrsxmet  22420  metdseq0  22465  elpi1i  22654  cphsqrtcl2  22794  tchcph  22844  lmmbrf  22868  caucfil  22889  lmclim  22909  cmsss  22955  srabn  22964  ovolfioo  23043  ovolficc  23044  elovolmr  23051  ovolctb  23065  ovolicc2lem3  23094  mbfmulc2lem  23220  mbfimaopnlem  23228  itg2mulclem  23319  iblrelem  23363  ellimc2  23447  mdegle0  23641  fta1glem2  23730  dgreq0  23825  plydivlem4  23855  plydivex  23856  fta1  23867  quotcan  23868  logeftb  24134  quad2  24366  cubic2  24375  dquartlem1  24378  atandm4  24406  fsumharmonic  24538  wilthlem1  24594  basellem8  24614  mumullem2  24706  chpchtsum  24744  logfaclbnd  24747  dchrelbas4  24768  lgsne0  24860  lgsqrlem2  24872  lgsdchrval  24879  lgsquadlem1  24905  lgsquadlem2  24906  2sqlem7  24949  dchrisum0lem1  25005  trgcgrg  25210  tgcgr4  25226  tgcolg  25249  lmiinv  25484  iseqlg  25547  eupath2lem3  26506  frgra3vlem2  26528  grpoid  26758  nvmeq0  26897  nvgt0  26913  imsmetlem  26929  nmlnogt0  27036  ip2eqi  27096  hvaddcan2  27312  hvmulcan2  27314  hvaddsub4  27319  hi2eq  27346  pjhtheu  27637  lnopeqi  28251  riesz1  28308  jpi  28513  chcv2  28599  cvp  28618  atnemeq0  28620  brabgaf  28800  fmptcof2  28839  funcnvmptOLD  28850  funcnvmpt  28851  nndiffz1  28936  nn0min  28954  xrge0addgt0  29022  smatrcl  29190  lmlim  29321  carsggect  29707  eulerpartlems  29749  eulerpartlemgh  29767  ballotlemfc0  29881  ballotlemfcc  29882  sgnneg  29929  signsvfpn  29988  signsvfnn  29989  bnj1280  30342  elmrsubrn  30671  msubff1  30707  fz0n  30869  imageval  31207  nn0prpwlem  31487  filnetlem4  31546  onsuct0  31610  onint1  31618  bj-mdiv  32334  dissneqlem  32363  wl-sbalnae  32524  wl-ax11-lem8  32548  wl-ax11-lem10  32550  sin2h  32569  tan2h  32571  matunitlindflem1  32575  matunitlindflem2  32576  matunitlindf  32577  poimirlem18  32597  poimirlem21  32600  poimirlem24  32603  heicant  32614  mblfinlem3  32618  ovoliunnfl  32621  voliunnfl  32623  volsupnfl  32624  mbfresfi  32626  mbfposadd  32627  itg2addnclem  32631  itg2addnclem2  32632  itg2addnc  32634  itg2gt0cn  32635  itgaddnclem2  32639  ftc1anclem5  32659  areacirclem1  32670  areacirclem4  32673  areacirc  32675  isdmn3  33043  lcvp  33345  lcv2  33347  lsatnem0  33350  atnem0  33623  cvlsupr2  33648  cvr2N  33715  athgt  33760  2llnmat  33828  pmap11  34066  pmapeq0  34070  2lnat  34088  paddclN  34146  pmapjat1  34157  ltrn2ateq  34485  dihcnvord  35581  dihcnv11  35582  dih0bN  35588  dih0sb  35592  dihlspsnat  35640  dihatexv2  35646  dihglblem6  35647  dochvalr  35664  dochn0nv  35682  djhcvat42  35722  dochsatshp  35758  dochshpsat  35761  dochkrsat2  35763  lcfl5a  35804  lcfl8a  35810  lclkrlem2a  35814  mapdcnvordN  35965  hdmap14lem4a  36181  hgmapeq0  36214  hdmaplkr  36223  hdmapellkr  36224  rmxycomplete  36500  gicabl  36687  ntrneiel  37399  ntrneik4w  37418  ntrneik4  37419  extoimad  37486  radcnvrat  37535  pm14.123b  37649  iotavalb  37653  climreeq  38680  clim2f  38703  clim2f2  38737  dfodd4  40109  oddprmne2  40162  pfxccat3a  40292  cusgruvtxb  40644  eupth2lem3lem3  41398  eupth2lem3lem6  41401  frgr3vlem2  41444  nnsgrpnmnd  41608  ovmpt2rdxf  41910