MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bitr3d Structured version   Visualization version   GIF version

Theorem bitr3d 268
Description: Deduction form of bitr3i 264. (Contributed by NM, 14-May-1993.)
Hypotheses
Ref Expression
bitr3d.1 (𝜑 → (𝜓𝜒))
bitr3d.2 (𝜑 → (𝜓𝜃))
Assertion
Ref Expression
bitr3d (𝜑 → (𝜒𝜃))

Proof of Theorem bitr3d
StepHypRef Expression
1 bitr3d.1 . . 3 (𝜑 → (𝜓𝜒))
21bicomd 211 . 2 (𝜑 → (𝜒𝜓))
3 bitr3d.2 . 2 (𝜑 → (𝜓𝜃))
42, 3bitrd 266 1 (𝜑 → (𝜒𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194
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 195
This theorem is referenced by:  3bitrrd  293  3bitr3d  296  3bitr3rd  297  biass  372  sbco2  2402  sbco3  2404  sbcom2  2432  sbal1  2447  sbal2  2448  sbal  2449  csbiebt  3518  prsspwg  4294  reusv2lem5  4793  copsex2t  4876  copsex2g  4877  ordtri2  5660  onmindif  5717  fnssresb  5902  fcnvres  5979  foelrni  6138  funimass5  6226  fmptco  6287  cbvfo  6421  isocnv  6457  isoini  6465  isoselem  6468  riota2df  6508  ovmpt2dxf  6661  caovcanrd  6712  onmindif2  6881  ordunisuc2  6913  dfom2  6936  ordge1n0  7442  ondif2  7446  oa00  7503  odi  7523  oeoe  7543  eceqoveq  7717  isfinite2  8080  unfilem1  8086  fodomfib  8102  inficl  8191  dffi3  8197  ordiso2  8280  ordtypelem9  8291  cantnfle  8428  cantnf  8450  wemapwe  8454  rankr1a  8559  bnd2  8616  iscard  8661  domtri2  8675  nnsdomel  8676  cardaleph  8772  dfac12lem2  8826  cfss  8947  axcc3  9120  fodomb  9206  iundom2g  9218  inar1  9453  ltpiord  9565  ordpinq  9621  suplem2pr  9731  enreceq  9743  subeq0  10158  negcon1  10184  subexsub  10300  subeqrev  10304  lesub  10358  ltsub13  10360  subge0  10392  mul0or  10518  mulcan1g  10531  div11  10564  divmuleq  10581  ltmuldiv2  10748  lemuldiv2  10755  nn1suc  10890  addltmul  11117  elnnnn0  11185  znn0sub  11259  prime  11292  zbtwnre  11620  xadddi2  11958  supxrbnd  11988  fz1n  12187  fzrev3  12233  fzo0n  12316  fzonlt0  12317  ico01fl0  12439  modsubdir  12558  om2uzlt2i  12569  hashf1lem1  13050  wrdlenge1n0  13143  cnpart  13776  sqrt11  13799  sqrtsq2  13805  absdiflt  13853  absdifle  13854  sqreulem  13895  sqreu  13896  eqsqrtor  13902  clim2  14031  climshft2  14109  isercoll  14194  sumrb  14239  supcvg  14375  prodrblem2  14448  sinbnd  14697  cosbnd  14698  sqrt2irr  14765  dvdscmulr  14796  dvdsmulcr  14797  oddm1even  14853  bitsmod  14944  bitsinv1lem  14949  qredeq  15157  cncongr2  15168  isprm3  15182  prmrp  15210  crth  15269  pcdvdsb  15359  pceq0  15361  unbenlem  15398  ramcl  15519  pwselbasb  15919  pwsle  15923  imasleval  15972  xpsfrnel2  15996  acsfn  16091  ismon2  16165  isepi2  16172  epii  16174  fthsect  16356  fthmon  16358  isipodrs  16932  ipodrsfi  16934  gsumval2a  17050  imasmnd2  17098  grpid  17228  grpidrcan  17251  grpidlcan  17252  grplmulf1o  17260  imasgrp2  17301  ghmeqker  17458  ghmf1  17460  gacan  17509  odmulgeq  17745  pgpssslw  17800  efgsfo  17923  efgred  17932  abladdsub4  17990  subgdmdprd  18204  imasring  18390  lspsnss2  18774  0ring01eqbi  19042  gsumbagdiaglem  19144  znf1o  19666  znfld  19675  znunit  19678  znrrg  19680  iporthcom  19746  ip2eq  19764  obsne0  19835  lindfmm  19932  lindsmm  19933  lsslinds  19936  eltg3  20524  eltop  20536  eltop2  20537  eltop3  20538  lmbrf  20821  cncnpi  20839  dfcon2  20979  1stcfb  21005  elptr  21133  xkoccn  21179  txcn  21186  hausdiag  21205  hmeoimaf1o  21330  isfbas  21390  ufileu  21480  alexsubALTlem4  21611  tsmsf1o  21705  ismet2  21895  imasdsf1olem  21935  imasf1oxmet  21937  imasf1omet  21938  xmseq0  22026  imasf1oxms  22051  metucn  22133  nrmmetd  22136  nmgt0  22191  nlmmul0or  22244  xrsxmet  22367  metdseq0  22412  elpi1i  22601  cphsqrtcl2  22738  tchcph  22788  lmmbrf  22812  caucfil  22833  lmclim  22853  cmsss  22899  srabn  22908  ovolfioo  22987  ovolficc  22988  elovolmr  22995  ovolctb  23009  ovolicc2lem3  23038  mbfmulc2lem  23164  mbfimaopnlem  23172  itg2mulclem  23263  iblrelem  23307  ellimc2  23391  mdegle0  23585  fta1glem2  23674  dgreq0  23769  plydivlem4  23799  plydivex  23800  fta1  23811  quotcan  23812  logeftb  24078  quad2  24310  cubic2  24319  dquartlem1  24322  atandm4  24350  fsumharmonic  24482  wilthlem1  24538  basellem8  24558  mumullem2  24650  chpchtsum  24688  logfaclbnd  24691  dchrelbas4  24712  lgsne0  24804  lgsqrlem2  24816  lgsdchrval  24823  lgsquadlem1  24849  lgsquadlem2  24850  2sqlem7  24893  dchrisum0lem1  24949  trgcgrg  25155  tgcgr4  25171  tgcolg  25194  lmiinv  25429  iseqlg  25492  eupath2lem3  26299  frgra3vlem2  26321  grpoid  26551  nvmeq0  26690  nvgt0  26706  imsmetlem  26722  nmlnogt0  26829  ip2eqi  26889  hvaddcan2  27105  hvmulcan2  27107  hvaddsub4  27112  hi2eq  27139  pjhtheu  27430  lnopeqi  28044  riesz1  28101  jpi  28306  chcv2  28392  cvp  28411  atnemeq0  28413  brabgaf  28593  fmptcof2  28632  funcnvmptOLD  28643  funcnvmpt  28644  nndiffz1  28729  nn0min  28747  xrge0addgt0  28815  smatrcl  28983  lmlim  29114  carsggect  29500  eulerpartlems  29542  eulerpartlemgh  29560  ballotlemfc0  29674  ballotlemfcc  29675  sgnneg  29722  signsvfpn  29781  signsvfnn  29782  bnj1280  30135  elmrsubrn  30464  msubff1  30500  fz0n  30662  imageval  31000  nn0prpwlem  31280  filnetlem4  31339  onsuct0  31403  onint1  31411  bj-mdiv  32117  dissneqlem  32146  wl-sbalnae  32307  wl-ax11-lem8  32331  wl-ax11-lem10  32333  sin2h  32352  tan2h  32354  matunitlindflem1  32358  matunitlindflem2  32359  matunitlindf  32360  poimirlem18  32380  poimirlem21  32383  poimirlem24  32386  heicant  32397  mblfinlem3  32401  ovoliunnfl  32404  voliunnfl  32406  volsupnfl  32407  mbfresfi  32409  mbfposadd  32410  itg2addnclem  32414  itg2addnclem2  32415  itg2addnc  32417  itg2gt0cn  32418  itgaddnclem2  32422  ftc1anclem5  32442  areacirclem1  32453  areacirclem4  32456  areacirc  32458  isdmn3  32826  lcvp  33128  lcv2  33130  lsatnem0  33133  atnem0  33406  cvlsupr2  33431  cvr2N  33498  athgt  33543  2llnmat  33611  pmap11  33849  pmapeq0  33853  2lnat  33871  paddclN  33929  pmapjat1  33940  ltrn2ateq  34268  dihcnvord  35364  dihcnv11  35365  dih0bN  35371  dih0sb  35375  dihlspsnat  35423  dihatexv2  35429  dihglblem6  35430  dochvalr  35447  dochn0nv  35465  djhcvat42  35505  dochsatshp  35541  dochshpsat  35544  dochkrsat2  35546  lcfl5a  35587  lcfl8a  35593  lclkrlem2a  35597  mapdcnvordN  35748  hdmap14lem4a  35964  hgmapeq0  35997  hdmaplkr  36006  hdmapellkr  36007  rmxycomplete  36283  gicabl  36470  ntrneiel  37182  ntrneik4w  37201  ntrneik4  37202  extoimad  37269  radcnvrat  37318  pm14.123b  37432  iotavalb  37436  climreeq  38463  clim2f  38486  clim2f2  38520  dfodd4  39893  oddprmne2  39946  pfxccat3a  40076  ssprss  40107  cusgruvtxb  40625  eupth2lem3lem3  41379  eupth2lem3lem6  41382  frgr3vlem2  41425  nnsgrpnmnd  41589  ovmpt2rdxf  41891
  Copyright terms: Public domain W3C validator