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 222	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜓))
3		bitr3d.2	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4	2, 3	bitrd 279	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  2162  19.21t  2200  19.23t  2204  sbco2  2511  sbco3  2513  sbal1  2528  sbal2  2529  clelab  2880  ceqsralt  3507  csbiebt  3923  prsspwg  4826  ssprss  4827  reusv2lem5  5400  copsex2t  5492  copsex2gOLD  5494  ordtri2  6397  onmindif  6454  fnssresb  6670  fcnvres  6766  foelcdmi  6951  funimass5  7054  fmptco  7124  cbvfo  7284  isocnv  7324  isoini  7332  isoselem  7335  riota2df  7386  ovmpodxf  7555  caovcanrd  7607  onmindif2  7792  ordunisuc2  7830  dfom2  7854  frxp2  8127  xpord2pred  8128  xpord3pred  8135  ordge1n0  8491  ondif2  8499  oa00  8556  odi  8576  oeoe  8596  eceqoveq  8813  isfinite2  9298  unfilem1  9307  fodomfib  9323  inficl  9417  dffi3  9423  ordiso2  9507  ordtypelem9  9518  cantnfle  9663  cantnf  9685  wemapwe  9689  rankr1a  9828  bnd2  9885  iscard  9967  domtri2  9981  nnsdomel  9982  cardaleph  10081  dfac12lem2  10136  cfss  10257  axcc3  10430  fodomb  10518  iundom2g  10532  inar1  10767  ltpiord  10879  ordpinq  10935  suplem2pr  11045  enreceq  11058  subeq0  11483  negcon1  11509  subexsub  11629  subeqrev  11633  lesub  11690  ltsub13  11692  subge0  11724  mul0or  11851  mulcan1g  11864  div11  11897  divmuleq  11916  mdiv  12047  ltmuldiv2  12085  lemuldiv2  12092  nn1suc  12231  addltmul  12445  elnnnn0  12512  znn0sub  12606  prime  12640  zbtwnre  12927  xadddi2  13273  supxrbnd  13304  fz1n  13516  fzrev3  13564  fzo0n  13651  fzonlt0  13652  ico01fl0  13781  divfl0  13786  modsubdir  13902  om2uzlt2i  13913  hashf1lem1  14412  hashf1lem1OLD  14413  wrdlenge1n0  14497  pfxccat3a  14685  cnpart  15184  sqrt11  15206  sqrtsq2  15212  absdiflt  15261  absdifle  15262  sqreulem  15303  sqreu  15304  eqsqrtor  15310  clim2  15445  climshft2  15523  isercoll  15611  sumrb  15656  supcvg  15799  prodrblem2  15872  sinbnd  16120  cosbnd  16121  sqrt2irr  16189  dvdscmulr  16225  dvdsmulcr  16226  oddm1even  16283  bitsmod  16374  bitsinv1lem  16379  qredeq  16591  cncongr2  16602  isprm3  16617  prmrp  16646  crth  16708  pcdvdsb  16799  pceq0  16801  unbenlem  16838  ramcl  16959  pwselbasb  17431  pwsle  17435  imasleval  17484  xpsfrnel2  17507  acsfn  17600  ismon2  17678  isepi2  17685  epii  17687  fthsect  17873  fthmon  17875  isipodrs  18487  ipodrsfi  18489  gsumval2a  18601  imasmnd2  18659  grpid  18857  grpidrcan  18885  grpidlcan  18886  grplmulf1o  18894  imasgrp2  18935  eqg0subg  19068  ghmeqker  19114  ghmf1  19116  gacan  19164  odmulgeq  19420  pgpssslw  19477  efgsfo  19602  efgred  19611  abladdsub4  19674  subgdmdprd  19899  imasring  20137  0ring01eqbi  20300  lspsnss2  20609  znf1o  21099  znfld  21108  znunit  21111  znrrg  21113  iporthcom  21180  ip2eq  21198  obsne0  21272  lindfmm  21374  lindsmm  21375  lsslinds  21378  gsumbagdiaglemOLD  21483  gsumbagdiaglem  21486  eltg3  22457  eltop  22469  eltop2  22470  eltop3  22471  lmbrf  22756  cncnpi  22774  dfconn2  22915  1stcfb  22941  elptr  23069  xkoccn  23115  txcn  23122  hausdiag  23141  hmeoimaf1o  23266  isfbas  23325  ufileu  23415  alexsubALTlem4  23546  tsmsf1o  23641  ismet2  23831  imasdsf1olem  23871  imasf1oxmet  23873  imasf1omet  23874  xmseq0  23962  imasf1oxms  23990  metucn  24072  nrmmetd  24075  nmgt0  24131  nlmmul0or  24192  xrsxmet  24317  metdseq0  24362  elpi1i  24554  cphsqrtcl2  24695  tcphcph  24746  lmmbrf  24771  caucfil  24792  lmclim  24812  cmsss  24860  srabn  24869  ovolfioo  24976  ovolficc  24977  elovolmr  24985  ovolctb  24999  ovolicc2lem3  25028  mbfmulc2lem  25156  mbfimaopnlem  25164  itg2mulclem  25256  iblrelem  25300  ellimc2  25386  mdegle0  25587  fta1glem2  25676  dgreq0  25771  plydivlem4  25801  plydivex  25802  fta1  25813  quotcan  25814  logeftb  26084  quad2  26334  cubic2  26343  dquartlem1  26346  atandm4  26374  fsumharmonic  26506  wilthlem1  26562  basellem8  26582  mumullem2  26674  chpchtsum  26712  logfaclbnd  26715  dchrelbas4  26736  lgsne0  26828  lgsqrlem2  26840  lgsdchrval  26847  lgsquadlem1  26873  lgsquadlem2  26874  2sqlem7  26917  addsqrexnreu  26935  dchrisum0lem1  27009  nogt01o  27189  slenlt  27245  addscan1  27467  mulscan2d  27621  mulscan1d  27622  sltmuldiv2wd  27639  trgcgrg  27756  tgcgr4  27772  tgcolg  27795  lmiinv  28033  iseqlg  28108  elntg2  28233  cusgruvtxb  28669  upgrewlkle2  28853  clwwlkn1  29284  eupth2lem3lem3  29473  eupth2lem3lem6  29476  frgr3vlem2  29517  grpoid  29761  nvmeq0  29899  nvgt0  29915  imsmetlem  29931  nmlnogt0  30038  ip2eqi  30097  hvaddcan2  30312  hvmulcan2  30314  hvaddsub4  30319  hi2eq  30346  pjhtheu  30635  lnopeqi  31249  riesz1  31306  jpi  31511  chcv2  31597  cvp  31616  atnemeq0  31618  brabgaf  31825  fmptcof2  31870  funcnvmpt  31880  nndiffz1  31985  nn0min  32014  xrge0addgt0  32180  lbslsp  32482  ressply1mon1p  32646  smatrcl  32765  lmlim  32916  carsggect  33306  eulerpartlems  33348  eulerpartlemgh  33366  ballotlemfc0  33480  ballotlemfcc  33481  sgnneg  33528  signsvfpn  33585  signsvfnn  33586  reprdifc  33628  bnj1280  34020  lfuhgr  34097  satffunlem1lem2  34383  elmrsubrn  34500  msubff1  34536  fz0n  34689  imageval  34891  nn0prpwlem  35196  filnetlem4  35255  onsuct0  35315  onint1  35323  dissneqlem  36210  fvineqsneu  36281  wl-sbalnae  36416  wl-ax11-lem8  36443  wl-ax11-lem10  36445  sin2h  36467  tan2h  36469  matunitlindflem1  36473  matunitlindflem2  36474  matunitlindf  36475  poimirlem18  36495  poimirlem21  36498  poimirlem24  36501  heicant  36512  mblfinlem3  36516  ovoliunnfl  36519  voliunnfl  36521  volsupnfl  36522  mbfresfi  36523  mbfposadd  36524  itg2addnclem  36528  itg2addnclem2  36529  itg2addnc  36531  itg2gt0cn  36532  itgaddnclem2  36536  ftc1anclem5  36554  areacirclem1  36565  areacirclem4  36568  areacirc  36570  isdmn3  36931  eldmres2  37132  cnvref4  37208  relbrcoss  37305  releldmqs  37517  lcvp  37899  lcv2  37901  lsatnem0  37904  atnem0  38177  cvlsupr2  38202  cvr2N  38271  athgt  38316  2llnmat  38384  pmap11  38622  pmapeq0  38626  2lnat  38644  paddclN  38702  pmapjat1  38713  ltrn2ateq  39040  dihcnvord  40134  dihcnv11  40135  dih0bN  40141  dih0sb  40145  dihlspsnat  40193  dihatexv2  40199  dihglblem6  40200  dochvalr  40217  dochn0nv  40235  djhcvat42  40275  dochsatshp  40311  dochshpsat  40314  dochkrsat2  40316  lcfl5a  40357  lcfl8a  40363  lclkrlem2a  40367  mapdcnvordN  40518  hdmap14lem4a  40731  hgmapeq0  40764  hdmaplkr  40773  hdmapellkr  40774  metakunt15  40988  frlmfielbas  41072  rmxycomplete  41642  gicabl  41827  minregex2  42272  ntrneiel  42818  ntrneik4w  42837  ntrneik4  42838  extoimad  42902  radcnvrat  43059  pm14.123b  43171  iotavalb  43175  infxrunb3  44121  climreeq  44316  clim2f  44339  clim2f2  44373  dfodd4  46314  oddprmne2  46370  nnsgrpnmnd  46575  imasrng  46665  ovmpordxf  46968  eenglngeehlnmlem2  47378  iscnrm3  47539