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

Theorem bitr3d 270
Description: Deduction form of bitr3i 266. (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 213 . 2 (𝜑 → (𝜒𝜓))
3 bitr3d.2 . 2 (𝜑 → (𝜓𝜃))
42, 3bitrd 268 1 (𝜑 → (𝜒𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
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 197
This theorem is referenced by:  3bitrrd  295  3bitr3d  298  3bitr3rd  299  biass  373  19.21t  2111  sbco2  2443  sbco3  2445  sbcom2  2473  sbal1  2488  sbal2  2489  sbal  2490  csbiebt  3586  prsspwg  4387  ssprss  4388  reusv2lem5  4903  copsex2t  4986  copsex2g  4987  ordtri2  5796  onmindif  5853  fnssresb  6041  fcnvres  6120  foelrni  6283  funimass5  6374  fmptco  6436  cbvfo  6584  isocnv  6620  isoini  6628  isoselem  6631  riota2df  6671  ovmpt2dxf  6828  caovcanrd  6879  onmindif2  7054  ordunisuc2  7086  dfom2  7109  ordge1n0  7623  ondif2  7627  oa00  7684  odi  7704  oeoe  7724  eceqoveq  7895  isfinite2  8259  unfilem1  8265  fodomfib  8281  inficl  8372  dffi3  8378  ordiso2  8461  ordtypelem9  8472  cantnfle  8606  cantnf  8628  wemapwe  8632  rankr1a  8737  bnd2  8794  iscard  8839  domtri2  8853  nnsdomel  8854  cardaleph  8950  dfac12lem2  9004  cfss  9125  axcc3  9298  fodomb  9386  iundom2g  9400  inar1  9635  ltpiord  9747  ordpinq  9803  suplem2pr  9913  enreceq  9925  subeq0  10345  negcon1  10371  subexsub  10487  subeqrev  10491  lesub  10545  ltsub13  10547  subge0  10579  mul0or  10705  mulcan1g  10718  div11  10751  divmuleq  10768  ltmuldiv2  10935  lemuldiv2  10942  nn1suc  11079  addltmul  11306  elnnnn0  11374  znn0sub  11462  prime  11496  zbtwnre  11824  xadddi2  12165  supxrbnd  12196  fz1n  12397  fzrev3  12444  fzo0n  12529  fzonlt0  12530  ico01fl0  12660  modsubdir  12779  om2uzlt2i  12790  hashf1lem1  13277  wrdlenge1n0  13372  ccat0  13394  cnpart  14024  sqrt11  14047  sqrtsq2  14053  absdiflt  14101  absdifle  14102  sqreulem  14143  sqreu  14144  eqsqrtor  14150  clim2  14279  climshft2  14357  isercoll  14442  sumrb  14488  supcvg  14632  prodrblem2  14705  sinbnd  14954  cosbnd  14955  sqrt2irr  15023  dvdscmulr  15057  dvdsmulcr  15058  oddm1even  15114  bitsmod  15205  bitsinv1lem  15210  qredeq  15418  cncongr2  15429  isprm3  15443  prmrp  15471  crth  15530  pcdvdsb  15620  pceq0  15622  unbenlem  15659  ramcl  15780  pwselbasb  16195  pwsle  16199  imasleval  16248  xpsfrnel2  16272  acsfn  16367  ismon2  16441  isepi2  16448  epii  16450  fthsect  16632  fthmon  16634  isipodrs  17208  ipodrsfi  17210  gsumval2a  17326  imasmnd2  17374  grpid  17504  grpidrcan  17527  grpidlcan  17528  grplmulf1o  17536  imasgrp2  17577  ghmeqker  17734  ghmf1  17736  gacan  17784  odmulgeq  18020  pgpssslw  18075  efgsfo  18198  efgred  18207  abladdsub4  18265  subgdmdprd  18479  imasring  18665  lspsnss2  19053  0ring01eqbi  19321  gsumbagdiaglem  19423  znf1o  19948  znfld  19957  znunit  19960  znrrg  19962  iporthcom  20028  ip2eq  20046  obsne0  20117  lindfmm  20214  lindsmm  20215  lsslinds  20218  eltg3  20814  eltop  20826  eltop2  20827  eltop3  20828  lmbrf  21112  cncnpi  21130  dfconn2  21270  1stcfb  21296  elptr  21424  xkoccn  21470  txcn  21477  hausdiag  21496  hmeoimaf1o  21621  isfbas  21680  ufileu  21770  alexsubALTlem4  21901  tsmsf1o  21995  ismet2  22185  imasdsf1olem  22225  imasf1oxmet  22227  imasf1omet  22228  xmseq0  22316  imasf1oxms  22341  metucn  22423  nrmmetd  22426  nmgt0  22481  nlmmul0or  22534  xrsxmet  22659  metdseq0  22704  elpi1i  22892  cphsqrtcl2  23032  tchcph  23082  lmmbrf  23106  caucfil  23127  lmclim  23147  cmsss  23193  srabn  23202  ovolfioo  23282  ovolficc  23283  elovolmr  23290  ovolctb  23304  ovolicc2lem3  23333  mbfmulc2lem  23459  mbfimaopnlem  23467  itg2mulclem  23558  iblrelem  23602  ellimc2  23686  mdegle0  23882  fta1glem2  23971  dgreq0  24066  plydivlem4  24096  plydivex  24097  fta1  24108  quotcan  24109  logeftb  24375  quad2  24611  cubic2  24620  dquartlem1  24623  atandm4  24651  fsumharmonic  24783  wilthlem1  24839  basellem8  24859  mumullem2  24951  chpchtsum  24989  logfaclbnd  24992  dchrelbas4  25013  lgsne0  25105  lgsqrlem2  25117  lgsdchrval  25124  lgsquadlem1  25150  lgsquadlem2  25151  2sqlem7  25194  dchrisum0lem1  25250  trgcgrg  25455  tgcgr4  25471  tgcolg  25494  lmiinv  25729  iseqlg  25792  cusgruvtxb  26374  clwwlkn1  27004  eupth2lem3lem3  27208  eupth2lem3lem6  27211  frgr3vlem2  27254  grpoid  27502  nvmeq0  27641  nvgt0  27657  imsmetlem  27673  nmlnogt0  27780  ip2eqi  27840  hvaddcan2  28056  hvmulcan2  28058  hvaddsub4  28063  hi2eq  28090  pjhtheu  28381  lnopeqi  28995  riesz1  29052  jpi  29257  chcv2  29343  cvp  29362  atnemeq0  29364  brabgaf  29546  fmptcof2  29585  funcnvmptOLD  29595  funcnvmpt  29596  nndiffz1  29676  nn0min  29695  xrge0addgt0  29819  smatrcl  29990  lmlim  30121  carsggect  30508  eulerpartlems  30550  eulerpartlemgh  30568  ballotlemfc0  30682  ballotlemfcc  30683  sgnneg  30730  signsvfpn  30790  signsvfnn  30791  reprdifc  30833  bnj1280  31214  elmrsubrn  31543  msubff1  31579  fz0n  31742  slenlt  32002  imageval  32162  nn0prpwlem  32442  filnetlem4  32501  onsuct0  32565  onint1  32573  bj-mdiv  33287  dissneqlem  33317  wl-sbalnae  33475  wl-ax11-lem8  33499  wl-ax11-lem10  33501  sin2h  33529  tan2h  33531  matunitlindflem1  33535  matunitlindflem2  33536  matunitlindf  33537  poimirlem18  33557  poimirlem21  33560  poimirlem24  33563  heicant  33574  mblfinlem3  33578  ovoliunnfl  33581  voliunnfl  33583  volsupnfl  33584  mbfresfi  33586  mbfposadd  33587  itg2addnclem  33591  itg2addnclem2  33592  itg2addnc  33594  itg2gt0cn  33595  itgaddnclem2  33599  ftc1anclem5  33619  areacirclem1  33630  areacirclem4  33633  areacirc  33635  isdmn3  34003  eldmres2  34179  relbrcoss  34336  lcvp  34645  lcv2  34647  lsatnem0  34650  atnem0  34923  cvlsupr2  34948  cvr2N  35015  athgt  35060  2llnmat  35128  pmap11  35366  pmapeq0  35370  2lnat  35388  paddclN  35446  pmapjat1  35457  ltrn2ateq  35785  dihcnvord  36880  dihcnv11  36881  dih0bN  36887  dih0sb  36891  dihlspsnat  36939  dihatexv2  36945  dihglblem6  36946  dochvalr  36963  dochn0nv  36981  djhcvat42  37021  dochsatshp  37057  dochshpsat  37060  dochkrsat2  37062  lcfl5a  37103  lcfl8a  37109  lclkrlem2a  37113  mapdcnvordN  37264  hdmap14lem4a  37480  hgmapeq0  37513  hdmaplkr  37522  hdmapellkr  37523  rmxycomplete  37799  gicabl  37986  ntrneiel  38696  ntrneik4w  38715  ntrneik4  38716  extoimad  38781  radcnvrat  38830  pm14.123b  38944  iotavalb  38948  infxrunb3  39964  climreeq  40163  clim2f  40186  clim2f2  40220  pfxccat3a  41754  dfodd4  41896  oddprmne2  41949  nnsgrpnmnd  42143  ovmpt2rdxf  42442
  Copyright terms: Public domain W3C validator