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  2174  19.21t  2207  19.23t  2211  sbco2  2519  sbco3  2521  sbal1  2536  sbal2  2537  clelab  2890  ceqsralt  3524  csbiebt  3951  prsspwg  4848  ssprss  4849  reusv2lem5  5420  copsex2t  5512  ordtri2  6430  onmindif  6487  fnssresb  6702  fcnvres  6798  foelcdmi  6983  funimass5  7088  fmptco  7163  cbvfo  7325  isocnv  7366  isoini  7374  isoselem  7377  riota2df  7428  ovmpodxf  7600  caovcanrd  7653  onmindif2  7843  ordunisuc2  7881  dfom2  7905  frxp2  8185  xpord2pred  8186  xpord3pred  8193  ordge1n0  8550  ondif2  8558  oa00  8615  odi  8635  oeoe  8655  eceqoveq  8880  isfinite2  9362  unfilem1  9371  fodomfib  9397  fodomfibOLD  9399  inficl  9494  dffi3  9500  ordiso2  9584  ordtypelem9  9595  cantnfle  9740  cantnf  9762  wemapwe  9766  rankr1a  9905  bnd2  9962  iscard  10044  domtri2  10058  nnsdomel  10059  cardaleph  10158  dfac12lem2  10214  cfss  10334  axcc3  10507  fodomb  10595  iundom2g  10609  inar1  10844  ltpiord  10956  ordpinq  11012  suplem2pr  11122  enreceq  11135  subeq0  11562  negcon1  11588  subexsub  11708  subeqrev  11712  lesub  11769  ltsub13  11771  subge0  11803  mul0or  11930  mulcan1g  11943  div11OLD  11978  divmuleq  11999  mdiv  12130  ltmuldiv2  12169  lemuldiv2  12176  nn1suc  12315  addltmul  12529  elnnnn0  12596  znn0sub  12690  prime  12724  zbtwnre  13011  xadddi2  13359  supxrbnd  13390  fz1n  13602  fzrev3  13650  fzo0n  13738  fzonlt0  13739  ico01fl0  13870  divfl0  13875  modsubdir  13991  om2uzlt2i  14002  hashf1lem1  14504  wrdlenge1n0  14598  pfxccat3a  14786  cnpart  15289  sqrt11  15311  sqrtsq2  15317  absdiflt  15366  absdifle  15367  sqreulem  15408  sqreu  15409  eqsqrtor  15415  clim2  15550  climshft2  15628  isercoll  15716  sumrb  15761  supcvg  15904  prodrblem2  15979  sinbnd  16228  cosbnd  16229  sqrt2irr  16297  dvdscmulr  16333  dvdsmulcr  16334  oddm1even  16391  bitsmod  16482  bitsinv1lem  16487  qredeq  16704  cncongr2  16715  isprm3  16730  prmrp  16759  crth  16825  pcdvdsb  16916  pceq0  16918  unbenlem  16955  ramcl  17076  pwselbasb  17548  pwsle  17552  imasleval  17601  xpsfrnel2  17624  acsfn  17717  ismon2  17795  isepi2  17802  epii  17804  fthsect  17992  fthmon  17994  isipodrs  18607  ipodrsfi  18609  gsumval2a  18723  imasmnd2  18809  grpid  19015  grpidrcan  19043  grpidlcan  19044  grplmulf1o  19053  grpraddf1o  19054  imasgrp2  19095  eqg0subg  19236  ghmeqker  19283  gacan  19345  odmulgeq  19599  pgpssslw  19656  efgsfo  19781  efgred  19790  abladdsub4  19853  subgdmdprd  20078  imasrng  20204  imasring  20353  0ring01eqbi  20558  domneq0r  20746  lspsnss2  21026  znf1o  21593  znfld  21602  znunit  21605  znrrg  21607  iporthcom  21676  ip2eq  21694  obsne0  21768  lindfmm  21870  lindsmm  21871  lsslinds  21874  gsumbagdiaglem  21973  psdmul  22193  eltg3  22990  eltop  23002  eltop2  23003  eltop3  23004  lmbrf  23289  cncnpi  23307  dfconn2  23448  1stcfb  23474  elptr  23602  xkoccn  23648  txcn  23655  hausdiag  23674  hmeoimaf1o  23799  isfbas  23858  ufileu  23948  alexsubALTlem4  24079  tsmsf1o  24174  ismet2  24364  imasdsf1olem  24404  imasf1oxmet  24406  imasf1omet  24407  xmseq0  24495  imasf1oxms  24523  metucn  24605  nrmmetd  24608  nmgt0  24664  nlmmul0or  24725  xrsxmet  24850  metdseq0  24895  elpi1i  25098  cphsqrtcl2  25239  tcphcph  25290  lmmbrf  25315  caucfil  25336  lmclim  25356  cmsss  25404  srabn  25413  ovolfioo  25521  ovolficc  25522  elovolmr  25530  ovolctb  25544  ovolicc2lem3  25573  mbfmulc2lem  25701  mbfimaopnlem  25709  itg2mulclem  25801  iblrelem  25846  ellimc2  25932  mdegle0  26136  fta1glem2  26228  dgreq0  26325  plydivlem4  26356  plydivex  26357  fta1  26368  quotcan  26369  logeftb  26643  quad2  26900  cubic2  26909  dquartlem1  26912  atandm4  26940  fsumharmonic  27073  wilthlem1  27129  basellem8  27149  mumullem2  27241  fsumdvdsmul  27256  chpchtsum  27281  logfaclbnd  27284  dchrelbas4  27305  lgsne0  27397  lgsqrlem2  27409  lgsdchrval  27416  lgsquadlem1  27442  lgsquadlem2  27443  2sqlem7  27486  addsqrexnreu  27504  dchrisum0lem1  27578  nogt01o  27759  slenlt  27815  addscan1  28045  mulscan2d  28223  mulscan1d  28224  muls0ord  28229  sltmuldiv2wd  28245  om2noseqlt2  28324  zn0subs  28407  trgcgrg  28541  tgcgr4  28557  tgcolg  28580  lmiinv  28818  iseqlg  28893  elntg2  29018  cusgruvtxb  29457  upgrewlkle2  29642  clwwlkn1  30073  eupth2lem3lem3  30262  eupth2lem3lem6  30265  frgr3vlem2  30306  grpoid  30552  nvmeq0  30690  nvgt0  30706  imsmetlem  30722  nmlnogt0  30829  ip2eqi  30888  hvaddcan2  31103  hvmulcan2  31105  hvaddsub4  31110  hi2eq  31137  pjhtheu  31426  lnopeqi  32040  riesz1  32097  jpi  32302  chcv2  32388  cvp  32407  atnemeq0  32409  brabgaf  32630  fmptcof2  32675  funcnvmpt  32685  nndiffz1  32791  nn0min  32824  xrge0addgt0  33003  lbslsp  33370  ressply1mon1p  33558  smatrcl  33742  lmlim  33893  carsggect  34283  eulerpartlems  34325  eulerpartlemgh  34343  ballotlemfc0  34457  ballotlemfcc  34458  sgnneg  34505  signsvfpn  34562  signsvfnn  34563  reprdifc  34604  bnj1280  34996  lfuhgr  35085  satffunlem1lem2  35371  elmrsubrn  35488  msubff1  35524  fz0n  35693  imageval  35894  nn0prpwlem  36288  filnetlem4  36347  onsuct0  36407  onint1  36415  dissneqlem  37306  fvineqsneu  37377  wl-sbalnae  37516  wl-ax11-lem8  37546  wl-ax11-lem10  37548  sin2h  37570  tan2h  37572  matunitlindflem1  37576  matunitlindflem2  37577  matunitlindf  37578  poimirlem18  37598  poimirlem21  37601  poimirlem24  37604  heicant  37615  mblfinlem3  37619  ovoliunnfl  37622  voliunnfl  37624  volsupnfl  37625  mbfresfi  37626  mbfposadd  37627  itg2addnclem  37631  itg2addnclem2  37632  itg2addnc  37634  itg2gt0cn  37635  itgaddnclem2  37639  ftc1anclem5  37657  areacirclem1  37668  areacirclem4  37671  areacirc  37673  isdmn3  38034  eldmres2  38231  cnvref4  38306  relbrcoss  38402  releldmqs  38614  lcvp  38996  lcv2  38998  lsatnem0  39001  atnem0  39274  cvlsupr2  39299  cvr2N  39368  athgt  39413  2llnmat  39481  pmap11  39719  pmapeq0  39723  2lnat  39741  paddclN  39799  pmapjat1  39810  ltrn2ateq  40137  dihcnvord  41231  dihcnv11  41232  dih0bN  41238  dih0sb  41242  dihlspsnat  41290  dihatexv2  41296  dihglblem6  41297  dochvalr  41314  dochn0nv  41332  djhcvat42  41372  dochsatshp  41408  dochshpsat  41411  dochkrsat2  41413  lcfl5a  41454  lcfl8a  41460  lclkrlem2a  41464  mapdcnvordN  41615  hdmap14lem4a  41828  hgmapeq0  41861  hdmaplkr  41870  hdmapellkr  41871  metakunt15  42176  cxp111d  42330  sn-ltmulgt11d  42438  frlmfielbas  42455  eu6w  42631  rmxycomplete  42874  gicabl  43056  minregex2  43497  ntrneiel  44043  ntrneik4w  44062  ntrneik4  44063  extoimad  44126  radcnvrat  44283  pm14.123b  44395  iotavalb  44399  infxrunb3  45339  climreeq  45534  clim2f  45557  clim2f2  45591  dfodd4  47533  oddprmne2  47589  nnsgrpnmnd  47901  ovmpordxf  48063  eenglngeehlnmlem2  48472  iscnrm3  48632