Theorem bitr3d 280

Description: Deduction form of bitr3i 276. (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 278	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  305  3bitr3d  308  3bitr3rd  309  biass  385  sbcom2  2161  19.21t  2199  19.23t  2203  sbco2  2510  sbco3  2512  sbal1  2527  sbal2  2528  clelab  2879  ceqsralt  3506  csbiebt  3923  prsspwg  4826  ssprss  4827  reusv2lem5  5400  copsex2t  5492  copsex2gOLD  5494  ordtri2  6399  onmindif  6456  fnssresb  6672  fcnvres  6768  foelcdmi  6953  funimass5  7056  fmptco  7129  cbvfo  7289  isocnv  7329  isoini  7337  isoselem  7340  riota2df  7391  ovmpodxf  7560  caovcanrd  7612  onmindif2  7797  ordunisuc2  7835  dfom2  7859  frxp2  8132  xpord2pred  8133  xpord3pred  8140  ordge1n0  8496  ondif2  8504  oa00  8561  odi  8581  oeoe  8601  eceqoveq  8818  isfinite2  9303  unfilem1  9312  fodomfib  9328  inficl  9422  dffi3  9428  ordiso2  9512  ordtypelem9  9523  cantnfle  9668  cantnf  9690  wemapwe  9694  rankr1a  9833  bnd2  9890  iscard  9972  domtri2  9986  nnsdomel  9987  cardaleph  10086  dfac12lem2  10141  cfss  10262  axcc3  10435  fodomb  10523  iundom2g  10537  inar1  10772  ltpiord  10884  ordpinq  10940  suplem2pr  11050  enreceq  11063  subeq0  11490  negcon1  11516  subexsub  11636  subeqrev  11640  lesub  11697  ltsub13  11699  subge0  11731  mul0or  11858  mulcan1g  11871  div11  11904  divmuleq  11923  mdiv  12054  ltmuldiv2  12092  lemuldiv2  12099  nn1suc  12238  addltmul  12452  elnnnn0  12519  znn0sub  12613  prime  12647  zbtwnre  12934  xadddi2  13280  supxrbnd  13311  fz1n  13523  fzrev3  13571  fzo0n  13658  fzonlt0  13659  ico01fl0  13788  divfl0  13793  modsubdir  13909  om2uzlt2i  13920  hashf1lem1  14419  hashf1lem1OLD  14420  wrdlenge1n0  14504  pfxccat3a  14692  cnpart  15191  sqrt11  15213  sqrtsq2  15219  absdiflt  15268  absdifle  15269  sqreulem  15310  sqreu  15311  eqsqrtor  15317  clim2  15452  climshft2  15530  isercoll  15618  sumrb  15663  supcvg  15806  prodrblem2  15879  sinbnd  16127  cosbnd  16128  sqrt2irr  16196  dvdscmulr  16232  dvdsmulcr  16233  oddm1even  16290  bitsmod  16381  bitsinv1lem  16386  qredeq  16598  cncongr2  16609  isprm3  16624  prmrp  16653  crth  16715  pcdvdsb  16806  pceq0  16808  unbenlem  16845  ramcl  16966  pwselbasb  17438  pwsle  17442  imasleval  17491  xpsfrnel2  17514  acsfn  17607  ismon2  17685  isepi2  17692  epii  17694  fthsect  17880  fthmon  17882  isipodrs  18494  ipodrsfi  18496  gsumval2a  18610  imasmnd2  18696  grpid  18896  grpidrcan  18924  grpidlcan  18925  grplmulf1o  18933  imasgrp2  18974  eqg0subg  19111  ghmeqker  19157  gacan  19210  odmulgeq  19466  pgpssslw  19523  efgsfo  19648  efgred  19657  abladdsub4  19720  subgdmdprd  19945  imasrng  20071  imasring  20218  0ring01eqbi  20421  lspsnss2  20760  znf1o  21326  znfld  21335  znunit  21338  znrrg  21340  iporthcom  21407  ip2eq  21425  obsne0  21499  lindfmm  21601  lindsmm  21602  lsslinds  21605  gsumbagdiaglemOLD  21710  gsumbagdiaglem  21713  eltg3  22685  eltop  22697  eltop2  22698  eltop3  22699  lmbrf  22984  cncnpi  23002  dfconn2  23143  1stcfb  23169  elptr  23297  xkoccn  23343  txcn  23350  hausdiag  23369  hmeoimaf1o  23494  isfbas  23553  ufileu  23643  alexsubALTlem4  23774  tsmsf1o  23869  ismet2  24059  imasdsf1olem  24099  imasf1oxmet  24101  imasf1omet  24102  xmseq0  24190  imasf1oxms  24218  metucn  24300  nrmmetd  24303  nmgt0  24359  nlmmul0or  24420  xrsxmet  24545  metdseq0  24590  elpi1i  24786  cphsqrtcl2  24927  tcphcph  24978  lmmbrf  25003  caucfil  25024  lmclim  25044  cmsss  25092  srabn  25101  ovolfioo  25208  ovolficc  25209  elovolmr  25217  ovolctb  25231  ovolicc2lem3  25260  mbfmulc2lem  25388  mbfimaopnlem  25396  itg2mulclem  25488  iblrelem  25532  ellimc2  25618  mdegle0  25819  fta1glem2  25908  dgreq0  26003  plydivlem4  26033  plydivex  26034  fta1  26045  quotcan  26046  logeftb  26316  quad2  26568  cubic2  26577  dquartlem1  26580  atandm4  26608  fsumharmonic  26740  wilthlem1  26796  basellem8  26816  mumullem2  26908  chpchtsum  26946  logfaclbnd  26949  dchrelbas4  26970  lgsne0  27062  lgsqrlem2  27074  lgsdchrval  27081  lgsquadlem1  27107  lgsquadlem2  27108  2sqlem7  27151  addsqrexnreu  27169  dchrisum0lem1  27243  nogt01o  27423  slenlt  27479  addscan1  27704  mulscan2d  27858  mulscan1d  27859  sltmuldiv2wd  27876  trgcgrg  28021  tgcgr4  28037  tgcolg  28060  lmiinv  28298  iseqlg  28373  elntg2  28498  cusgruvtxb  28934  upgrewlkle2  29118  clwwlkn1  29549  eupth2lem3lem3  29738  eupth2lem3lem6  29741  frgr3vlem2  29782  grpoid  30028  nvmeq0  30166  nvgt0  30182  imsmetlem  30198  nmlnogt0  30305  ip2eqi  30364  hvaddcan2  30579  hvmulcan2  30581  hvaddsub4  30586  hi2eq  30613  pjhtheu  30902  lnopeqi  31516  riesz1  31573  jpi  31778  chcv2  31864  cvp  31883  atnemeq0  31885  brabgaf  32092  fmptcof2  32137  funcnvmpt  32147  nndiffz1  32252  nn0min  32281  xrge0addgt0  32447  lbslsp  32755  ressply1mon1p  32919  smatrcl  33062  lmlim  33213  carsggect  33603  eulerpartlems  33645  eulerpartlemgh  33663  ballotlemfc0  33777  ballotlemfcc  33778  sgnneg  33825  signsvfpn  33882  signsvfnn  33883  reprdifc  33925  bnj1280  34317  lfuhgr  34394  satffunlem1lem2  34680  elmrsubrn  34797  msubff1  34833  fz0n  34992  imageval  35194  nn0prpwlem  35510  filnetlem4  35569  onsuct0  35629  onint1  35637  dissneqlem  36524  fvineqsneu  36595  wl-sbalnae  36730  wl-ax11-lem8  36757  wl-ax11-lem10  36759  sin2h  36781  tan2h  36783  matunitlindflem1  36787  matunitlindflem2  36788  matunitlindf  36789  poimirlem18  36809  poimirlem21  36812  poimirlem24  36815  heicant  36826  mblfinlem3  36830  ovoliunnfl  36833  voliunnfl  36835  volsupnfl  36836  mbfresfi  36837  mbfposadd  36838  itg2addnclem  36842  itg2addnclem2  36843  itg2addnc  36845  itg2gt0cn  36846  itgaddnclem2  36850  ftc1anclem5  36868  areacirclem1  36879  areacirclem4  36882  areacirc  36884  isdmn3  37245  eldmres2  37446  cnvref4  37522  relbrcoss  37619  releldmqs  37831  lcvp  38213  lcv2  38215  lsatnem0  38218  atnem0  38491  cvlsupr2  38516  cvr2N  38585  athgt  38630  2llnmat  38698  pmap11  38936  pmapeq0  38940  2lnat  38958  paddclN  39016  pmapjat1  39027  ltrn2ateq  39354  dihcnvord  40448  dihcnv11  40449  dih0bN  40455  dih0sb  40459  dihlspsnat  40507  dihatexv2  40513  dihglblem6  40514  dochvalr  40531  dochn0nv  40549  djhcvat42  40589  dochsatshp  40625  dochshpsat  40628  dochkrsat2  40630  lcfl5a  40671  lcfl8a  40677  lclkrlem2a  40681  mapdcnvordN  40832  hdmap14lem4a  41045  hgmapeq0  41078  hdmaplkr  41087  hdmapellkr  41088  metakunt15  41305  frlmfielbas  41380  rmxycomplete  41958  gicabl  42143  minregex2  42588  ntrneiel  43134  ntrneik4w  43153  ntrneik4  43154  extoimad  43218  radcnvrat  43375  pm14.123b  43487  iotavalb  43491  infxrunb3  44433  climreeq  44628  clim2f  44651  clim2f2  44685  dfodd4  46626  oddprmne2  46682  nnsgrpnmnd  46855  ovmpordxf  47103  eenglngeehlnmlem2  47512  iscnrm3  47673