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  5337  copsex2t  5438  ordtri2  6350  onmindif  6409  fnssresb  6612  fcnvres  6709  foelcdmi  6893  funcnvmpt  6941  funimass5  6999  fmptco  7074  cbvfo  7235  isocnv  7276  isoini  7284  isoselem  7287  riota2df  7338  ovmpodxf  7508  caovcanrd  7561  onmindif2  7752  ordunisuc2  7786  dfom2  7810  frxp2  8085  xpord2pred  8086  xpord3pred  8093  ordge1n0  8420  ondif2  8428  oa00  8485  odi  8505  oeoe  8526  eceqoveq  8760  isfinite2  9199  unfilem1  9206  fodomfib  9230  fodomfibOLD  9232  inficl  9329  dffi3  9335  ordiso2  9421  ordtypelem9  9432  cantnfle  9581  cantnf  9603  wemapwe  9607  rankr1a  9749  bnd2  9806  iscard  9888  domtri2  9902  nnsdomel  9903  cardaleph  10000  dfac12lem2  10056  cfss  10176  axcc3  10349  fodomb  10437  iundom2g  10451  inar1  10687  ltpiord  10799  ordpinq  10855  suplem2pr  10965  enreceq  10978  subeq0  11408  negcon1  11434  subexsub  11556  subeqrev  11560  lesub  11617  ltsub13  11619  subge0  11651  mul0or  11778  mulcan1g  11791  div11OLD  11826  divmuleq  11847  mdiv  11978  ltmuldiv2  12017  lemuldiv2  12024  nn1suc  12168  addltmul  12378  elnnnn0  12445  znn0sub  12539  prime  12574  zbtwnre  12860  xadddi2  13213  supxrbnd  13244  fz1n  13459  fzrev3  13507  fzo0n  13598  fzonlt0  13599  ico01fl0  13740  divfl0  13745  modaddid  13831  modsubdir  13864  om2uzlt2i  13875  hashf1lem1  14379  wrdlenge1n0  14474  pfxccat3a  14662  cnpart  15164  sqrt11  15186  sqrtsq2  15192  absdiflt  15242  absdifle  15243  sqreulem  15284  sqreu  15285  eqsqrtor  15291  clim2  15428  climshft2  15506  isercoll  15592  sumrb  15637  supcvg  15780  prodrblem2  15855  sinbnd  16106  cosbnd  16107  sqrt2irr  16175  dvdscmulr  16212  dvdsmulcr  16213  oddm1even  16271  bitsmod  16364  bitsinv1lem  16369  qredeq  16585  cncongr2  16596  isprm3  16611  prmrp  16640  crth  16706  pcdvdsb  16798  pceq0  16800  unbenlem  16837  ramcl  16958  pwselbasb  17409  pwsle  17414  imasleval  17463  xpsfrnel2  17486  acsfn  17583  ismon2  17659  isepi2  17666  epii  17668  fthsect  17852  fthmon  17854  isipodrs  18461  ipodrsfi  18463  gsumval2a  18611  imasmnd2  18700  grpid  18909  grpidrcan  18937  grpidlcan  18938  grplmulf1o  18947  grpraddf1o  18948  imasgrp2  18989  eqg0subg  19129  ghmeqker  19176  gacan  19238  odmulgeq  19490  pgpssslw  19547  efgsfo  19672  efgred  19681  abladdsub4  19744  subgdmdprd  19969  imasrng  20116  imasring  20268  0ring01eqbi  20467  domneq0r  20659  lspsnss2  20958  znf1o  21508  znfld  21517  znunit  21520  znrrg  21522  iporthcom  21592  ip2eq  21610  obsne0  21682  lindfmm  21784  lindsmm  21785  lsslinds  21788  gsumbagdiaglem  21887  psdmul  22110  eltg3  22905  eltop  22917  eltop2  22918  eltop3  22919  lmbrf  23203  cncnpi  23221  dfconn2  23362  1stcfb  23388  elptr  23516  xkoccn  23562  txcn  23569  hausdiag  23588  hmeoimaf1o  23713  isfbas  23772  ufileu  23862  alexsubALTlem4  23993  tsmsf1o  24088  ismet2  24276  imasdsf1olem  24316  imasf1oxmet  24318  imasf1omet  24319  xmseq0  24407  imasf1oxms  24432  metucn  24514  nrmmetd  24517  nmgt0  24573  nlmmul0or  24626  xrsxmet  24753  metdseq0  24798  elpi1i  24991  cphsqrtcl2  25131  tcphcph  25182  lmmbrf  25207  caucfil  25228  lmclim  25248  cmsss  25296  srabn  25305  ovolfioo  25412  ovolficc  25413  elovolmr  25421  ovolctb  25435  ovolicc2lem3  25464  mbfmulc2lem  25592  mbfimaopnlem  25600  itg2mulclem  25691  iblrelem  25736  ellimc2  25822  mdegle0  26023  fta1glem2  26115  dgreq0  26211  plydivlem4  26244  plydivex  26245  fta1  26256  quotcan  26257  logeftb  26532  quad2  26789  cubic2  26798  dquartlem1  26801  atandm4  26829  fsumharmonic  26962  wilthlem1  27018  basellem8  27038  mumullem2  27130  fsumdvdsmul  27145  chpchtsum  27170  logfaclbnd  27173  dchrelbas4  27194  lgsne0  27286  lgsqrlem2  27298  lgsdchrval  27305  lgsquadlem1  27331  lgsquadlem2  27332  2sqlem7  27375  addsqrexnreu  27393  dchrisum0lem1  27467  nogt01o  27648  lenlts  27704  addscan1  27974  subseq0d  28085  mulscan2d  28159  mulscan1d  28160  muls0ord  28165  ltmuldivs2wd  28182  onnolt  28246  onlts  28247  om2noseqlt2  28280  zn0subs  28383  bdaypw2n0bndlem  28443  bdayfinbndlem1  28447  trgcgrg  28571  tgcgr4  28587  tgcolg  28610  lmiinv  28848  iseqlg  28923  elntg2  29042  cusgruvtxb  29479  upgrewlkle2  29664  clwwlkn1  30100  eupth2lem3lem3  30289  eupth2lem3lem6  30292  frgr3vlem2  30333  grpoid  30580  nvmeq0  30718  nvgt0  30734  imsmetlem  30750  nmlnogt0  30857  ip2eqi  30916  hvaddcan2  31131  hvmulcan2  31133  hvaddsub4  31138  hi2eq  31165  pjhtheu  31454  lnopeqi  32068  riesz1  32125  jpi  32330  chcv2  32416  cvp  32435  atnemeq0  32437  brabgaf  32668  fmptcof2  32719  nndiffz1  32849  nn0min  32884  sgnneg  32897  xrge0addgt0  33082  lbslsp  33442  ressply1mon1p  33633  fldextrspunlsplem  33823  smatrcl  33946  lmlim  34097  carsggect  34468  eulerpartlems  34510  eulerpartlemgh  34528  ballotlemfc0  34643  ballotlemfcc  34644  signsvfpn  34735  signsvfnn  34736  reprdifc  34777  bnj1280  35168  fineqvnttrclselem3  35273  lfuhgr  35306  satffunlem1lem2  35591  elmrsubrn  35708  msubff1  35744  fz0n  35919  imageval  36116  nn0prpwlem  36510  filnetlem4  36569  onsuct0  36629  onint1  36637  dissneqlem  37652  fvineqsneu  37723  wl-sbalnae  37878  sin2h  37922  tan2h  37924  matunitlindflem1  37928  matunitlindflem2  37929  matunitlindf  37930  poimirlem18  37950  poimirlem21  37953  poimirlem24  37956  heicant  37967  mblfinlem3  37971  ovoliunnfl  37974  voliunnfl  37976  volsupnfl  37977  mbfresfi  37978  mbfposadd  37979  itg2addnclem  37983  itg2addnclem2  37984  itg2addnc  37986  itg2gt0cn  37987  itgaddnclem2  37991  ftc1anclem5  38009  areacirclem1  38020  areacirclem4  38023  areacirc  38025  isdmn3  38386  eldmres2  38594  cnvref4  38662  relbrcoss  38848  releldmqs  39055  lcvp  39477  lcv2  39479  lsatnem0  39482  atnem0  39755  cvlsupr2  39780  cvr2N  39848  athgt  39893  2llnmat  39961  pmap11  40199  pmapeq0  40203  2lnat  40221  paddclN  40279  pmapjat1  40290  ltrn2ateq  40617  dihcnvord  41711  dihcnv11  41712  dih0bN  41718  dih0sb  41722  dihlspsnat  41770  dihatexv2  41776  dihglblem6  41777  dochvalr  41794  dochn0nv  41812  djhcvat42  41852  dochsatshp  41888  dochshpsat  41891  dochkrsat2  41893  lcfl5a  41934  lcfl8a  41940  lclkrlem2a  41944  mapdcnvordN  42095  hdmap14lem4a  42308  hgmapeq0  42341  hdmaplkr  42350  hdmapellkr  42351  cxp111d  42773  sn-remul0ord  42839  sn-ltmulgt11d  42918  frlmfielbas  42944  eu6w  43108  rmxycomplete  43348  gicabl  43530  minregex2  43965  ntrneiel  44511  ntrneik4w  44530  ntrneik4  44531  extoimad  44594  radcnvrat  44744  pm14.123b  44856  iotavalb  44860  infxrunb3  45856  climreeq  46047  clim2f  46068  clim2f2  46102  dfodd4  48093  oddprmne2  48149  nnsgrpnmnd  48612  ovmpordxf  48773  eenglngeehlnmlem2  49172  iscnrm3  49385  uptrlem1  49643