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  3924  prsspwg  4827  ssprss  4828  reusv2lem5  5401  copsex2t  5493  copsex2gOLD  5495  ordtri2  6400  onmindif  6457  fnssresb  6673  fcnvres  6769  foelcdmi  6954  funimass5  7057  fmptco  7127  cbvfo  7287  isocnv  7327  isoini  7335  isoselem  7338  riota2df  7389  ovmpodxf  7558  caovcanrd  7610  onmindif2  7795  ordunisuc2  7833  dfom2  7857  frxp2  8130  xpord2pred  8131  xpord3pred  8138  ordge1n0  8494  ondif2  8502  oa00  8559  odi  8579  oeoe  8599  eceqoveq  8816  isfinite2  9301  unfilem1  9310  fodomfib  9326  inficl  9420  dffi3  9426  ordiso2  9510  ordtypelem9  9521  cantnfle  9666  cantnf  9688  wemapwe  9692  rankr1a  9831  bnd2  9888  iscard  9970  domtri2  9984  nnsdomel  9985  cardaleph  10084  dfac12lem2  10139  cfss  10260  axcc3  10433  fodomb  10521  iundom2g  10535  inar1  10770  ltpiord  10882  ordpinq  10938  suplem2pr  11048  enreceq  11061  subeq0  11486  negcon1  11512  subexsub  11632  subeqrev  11636  lesub  11693  ltsub13  11695  subge0  11727  mul0or  11854  mulcan1g  11867  div11  11900  divmuleq  11919  mdiv  12050  ltmuldiv2  12088  lemuldiv2  12095  nn1suc  12234  addltmul  12448  elnnnn0  12515  znn0sub  12609  prime  12643  zbtwnre  12930  xadddi2  13276  supxrbnd  13307  fz1n  13519  fzrev3  13567  fzo0n  13654  fzonlt0  13655  ico01fl0  13784  divfl0  13789  modsubdir  13905  om2uzlt2i  13916  hashf1lem1  14415  hashf1lem1OLD  14416  wrdlenge1n0  14500  pfxccat3a  14688  cnpart  15187  sqrt11  15209  sqrtsq2  15215  absdiflt  15264  absdifle  15265  sqreulem  15306  sqreu  15307  eqsqrtor  15313  clim2  15448  climshft2  15526  isercoll  15614  sumrb  15659  supcvg  15802  prodrblem2  15875  sinbnd  16123  cosbnd  16124  sqrt2irr  16192  dvdscmulr  16228  dvdsmulcr  16229  oddm1even  16286  bitsmod  16377  bitsinv1lem  16382  qredeq  16594  cncongr2  16605  isprm3  16620  prmrp  16649  crth  16711  pcdvdsb  16802  pceq0  16804  unbenlem  16841  ramcl  16962  pwselbasb  17434  pwsle  17438  imasleval  17487  xpsfrnel2  17510  acsfn  17603  ismon2  17681  isepi2  17688  epii  17690  fthsect  17876  fthmon  17878  isipodrs  18490  ipodrsfi  18492  gsumval2a  18604  imasmnd2  18662  grpid  18860  grpidrcan  18888  grpidlcan  18889  grplmulf1o  18897  imasgrp2  18938  eqg0subg  19073  ghmeqker  19119  ghmf1  19121  gacan  19169  odmulgeq  19425  pgpssslw  19482  efgsfo  19607  efgred  19616  abladdsub4  19679  subgdmdprd  19904  imasring  20143  0ring01eqbi  20307  lspsnss2  20616  znf1o  21107  znfld  21116  znunit  21119  znrrg  21121  iporthcom  21188  ip2eq  21206  obsne0  21280  lindfmm  21382  lindsmm  21383  lsslinds  21386  gsumbagdiaglemOLD  21491  gsumbagdiaglem  21494  eltg3  22465  eltop  22477  eltop2  22478  eltop3  22479  lmbrf  22764  cncnpi  22782  dfconn2  22923  1stcfb  22949  elptr  23077  xkoccn  23123  txcn  23130  hausdiag  23149  hmeoimaf1o  23274  isfbas  23333  ufileu  23423  alexsubALTlem4  23554  tsmsf1o  23649  ismet2  23839  imasdsf1olem  23879  imasf1oxmet  23881  imasf1omet  23882  xmseq0  23970  imasf1oxms  23998  metucn  24080  nrmmetd  24083  nmgt0  24139  nlmmul0or  24200  xrsxmet  24325  metdseq0  24370  elpi1i  24562  cphsqrtcl2  24703  tcphcph  24754  lmmbrf  24779  caucfil  24800  lmclim  24820  cmsss  24868  srabn  24877  ovolfioo  24984  ovolficc  24985  elovolmr  24993  ovolctb  25007  ovolicc2lem3  25036  mbfmulc2lem  25164  mbfimaopnlem  25172  itg2mulclem  25264  iblrelem  25308  ellimc2  25394  mdegle0  25595  fta1glem2  25684  dgreq0  25779  plydivlem4  25809  plydivex  25810  fta1  25821  quotcan  25822  logeftb  26092  quad2  26344  cubic2  26353  dquartlem1  26356  atandm4  26384  fsumharmonic  26516  wilthlem1  26572  basellem8  26592  mumullem2  26684  chpchtsum  26722  logfaclbnd  26725  dchrelbas4  26746  lgsne0  26838  lgsqrlem2  26850  lgsdchrval  26857  lgsquadlem1  26883  lgsquadlem2  26884  2sqlem7  26927  addsqrexnreu  26945  dchrisum0lem1  27019  nogt01o  27199  slenlt  27255  addscan1  27477  mulscan2d  27631  mulscan1d  27632  sltmuldiv2wd  27649  trgcgrg  27766  tgcgr4  27782  tgcolg  27805  lmiinv  28043  iseqlg  28118  elntg2  28243  cusgruvtxb  28679  upgrewlkle2  28863  clwwlkn1  29294  eupth2lem3lem3  29483  eupth2lem3lem6  29486  frgr3vlem2  29527  grpoid  29773  nvmeq0  29911  nvgt0  29927  imsmetlem  29943  nmlnogt0  30050  ip2eqi  30109  hvaddcan2  30324  hvmulcan2  30326  hvaddsub4  30331  hi2eq  30358  pjhtheu  30647  lnopeqi  31261  riesz1  31318  jpi  31523  chcv2  31609  cvp  31628  atnemeq0  31630  brabgaf  31837  fmptcof2  31882  funcnvmpt  31892  nndiffz1  31997  nn0min  32026  xrge0addgt0  32192  lbslsp  32493  ressply1mon1p  32657  smatrcl  32776  lmlim  32927  carsggect  33317  eulerpartlems  33359  eulerpartlemgh  33377  ballotlemfc0  33491  ballotlemfcc  33492  sgnneg  33539  signsvfpn  33596  signsvfnn  33597  reprdifc  33639  bnj1280  34031  lfuhgr  34108  satffunlem1lem2  34394  elmrsubrn  34511  msubff1  34547  fz0n  34700  imageval  34902  nn0prpwlem  35207  filnetlem4  35266  onsuct0  35326  onint1  35334  dissneqlem  36221  fvineqsneu  36292  wl-sbalnae  36427  wl-ax11-lem8  36454  wl-ax11-lem10  36456  sin2h  36478  tan2h  36480  matunitlindflem1  36484  matunitlindflem2  36485  matunitlindf  36486  poimirlem18  36506  poimirlem21  36509  poimirlem24  36512  heicant  36523  mblfinlem3  36527  ovoliunnfl  36530  voliunnfl  36532  volsupnfl  36533  mbfresfi  36534  mbfposadd  36535  itg2addnclem  36539  itg2addnclem2  36540  itg2addnc  36542  itg2gt0cn  36543  itgaddnclem2  36547  ftc1anclem5  36565  areacirclem1  36576  areacirclem4  36579  areacirc  36581  isdmn3  36942  eldmres2  37143  cnvref4  37219  relbrcoss  37316  releldmqs  37528  lcvp  37910  lcv2  37912  lsatnem0  37915  atnem0  38188  cvlsupr2  38213  cvr2N  38282  athgt  38327  2llnmat  38395  pmap11  38633  pmapeq0  38637  2lnat  38655  paddclN  38713  pmapjat1  38724  ltrn2ateq  39051  dihcnvord  40145  dihcnv11  40146  dih0bN  40152  dih0sb  40156  dihlspsnat  40204  dihatexv2  40210  dihglblem6  40211  dochvalr  40228  dochn0nv  40246  djhcvat42  40286  dochsatshp  40322  dochshpsat  40325  dochkrsat2  40327  lcfl5a  40368  lcfl8a  40374  lclkrlem2a  40378  mapdcnvordN  40529  hdmap14lem4a  40742  hgmapeq0  40775  hdmaplkr  40784  hdmapellkr  40785  metakunt15  40999  frlmfielbas  41074  rmxycomplete  41656  gicabl  41841  minregex2  42286  ntrneiel  42832  ntrneik4w  42851  ntrneik4  42852  extoimad  42916  radcnvrat  43073  pm14.123b  43185  iotavalb  43189  infxrunb3  44134  climreeq  44329  clim2f  44352  clim2f2  44386  dfodd4  46327  oddprmne2  46383  nnsgrpnmnd  46588  imasrng  46678  ovmpordxf  47014  eenglngeehlnmlem2  47424  iscnrm3  47585