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

Theorem bitr4d 271
Description: Deduction form of bitr4i 267. (Contributed by NM, 30-Jun-1993.)
Hypotheses
Ref Expression
bitr4d.1 (𝜑 → (𝜓𝜒))
bitr4d.2 (𝜑 → (𝜃𝜒))
Assertion
Ref Expression
bitr4d (𝜑 → (𝜓𝜃))

Proof of Theorem bitr4d
StepHypRef Expression
1 bitr4d.1 . 2 (𝜑 → (𝜓𝜒))
2 bitr4d.2 . . 3 (𝜑 → (𝜃𝜒))
32bicomd 213 . 2 (𝜑 → (𝜒𝜃))
41, 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:  3bitr2d  296  3bitr2rd  297  3bitr4d  300  3bitr4rd  301  mpbirand  529  bianabs  942  sbcom3  2439  sbal1  2488  sbal2  2489  issn  4395  disjprg  4680  reuhypd  4925  ordtri3  5797  ordsssuc  5850  iota1  5903  funbrfv2b  6279  dffn5  6280  feqmptdf  6290  dmfco  6311  fneqeql  6365  f1ompt  6422  dff13  6552  fliftcnv  6601  soisores  6617  isotr  6626  isoini  6628  caovord3  6889  releldm2  7262  brtpos  7406  tpostpos  7417  oe1m  7670  oawordri  7675  oalimcl  7685  omlimcl  7703  omabs  7772  iserd  7813  qliftel  7873  qliftfun  7875  qliftf  7878  ecopovsym  7892  pw2f1olem  8105  mapen  8165  suppeqfsuppbi  8330  funsnfsupp  8340  mapfien  8354  supisolem  8420  cantnflem1  8624  wemapwe  8632  rankr1clem  8721  rankr1c  8722  ranklim  8745  r1pwALT  8747  r1pwcl  8748  isfin1-2  9245  isfin1-4  9247  fin71num  9257  axdc3lem2  9311  ltmnq  9832  prlem936  9907  ltsosr  9953  ltasr  9959  xrlenlt  10141  ltxrlt  10146  letri3  10161  ne0gt0  10180  subadd  10322  ltsubadd2  10537  lesubadd2  10539  suble  10544  ltsub23  10546  ltaddpos2  10557  ltsubpos  10558  subge02  10582  ltord2  10595  leord2  10596  ltaddsublt  10692  divmul  10726  divmul3  10728  rec11r  10762  ltdiv1  10925  ltdivmul2  10938  ledivmul2  10940  ltrec  10943  ltdiv2  10947  negfi  11009  negiso  11041  nnle1eq1  11086  avgle1  11310  avgle2  11311  avgle  11312  nn0le0eq0  11359  elz2  11432  znnnlt1  11442  zleltp1  11466  uzin  11758  difrp  11906  xrltlen  12017  dfle2  12018  xrletri3  12023  xgepnf  12034  xlemnf  12036  qbtwnre  12068  xltnegi  12085  supxrre  12195  supxrre1  12198  infxrre  12204  ixxun  12229  elioo5  12269  elfz5  12372  elfzm11  12449  uzsplit  12450  predfz  12503  flbi  12657  flbi2  12658  fldiv4lem1div2uz2  12677  fznnfl  12701  zmodid2  12738  2submod  12771  lt2sq  12977  le2sq  12978  sqlecan  13011  bcval5  13145  shftfib  13856  mulre  13905  cnpart  14024  sqrlem6  14032  sqrmo  14036  elicc4abs  14103  abs2difabs  14118  cau4  14140  limsupgre  14256  clim2  14279  ello12  14291  ello1mpt2  14297  elo12  14302  lo1resb  14339  o1resb  14341  climeq  14342  climmpt2  14348  isercoll  14442  caucvgb  14454  fsumss  14500  fsumabs  14577  isumshft  14615  geomulcvg  14651  fprodss  14722  absefib  14972  dvdsval3  15031  dvdsabseq  15082  dvdsflip  15086  dvdsssfz1  15087  mod2eq1n2dvds  15118  ndvdsadd  15181  bitscmp  15207  smupvallem  15252  dvdssq  15327  lcmdvds  15368  ncoprmgcdgt1b  15411  coprmdvdsOLD  15414  isprm3  15443  isprm5  15466  phiprmpw  15528  prmdiv  15537  pc11  15631  pcz  15632  pockthlem  15656  prmreclem2  15668  prmreclem4  15670  prmreclem6  15672  1arith  15678  vdwapun  15725  ramval  15759  rami  15766  ramcl  15780  pwsle  16199  ercpbllem  16255  invsym  16469  funcres2c  16608  latnle  17132  grpinvcnv  17530  subgacs  17676  eqger  17691  gexdvds2  18046  pgpfi1  18056  pgpfi  18066  lsmass  18129  lssnle  18133  lsmdisj3b  18149  lsmhash  18164  ablsubadd  18263  gsumval3lem2  18353  subgdmdprd  18479  pgpfac1lem2  18520  dvdsr02  18702  drngid2  18811  issubrg3  18856  lssacs  19015  lspsnel5  19043  psrbaglefi  19420  coe1mul2lem1  19685  prmirred  19891  chrdvds  19924  chrcong  19925  chrnzr  19926  znleval  19951  znleval2  19952  cygznlem3  19966  frlmbas  20147  elfilspd  20190  lindfmm  20214  islindf4  20225  islindf5  20226  mdetunilem9  20474  discld  20941  isneip  20957  neiptopnei  20984  lpdifsn  20995  restopnb  21027  restopn2  21029  restdis  21030  restperf  21036  lmbr2  21111  cncls2  21125  cnprest  21141  cnprest2  21142  iscnrm2  21190  ist0-2  21196  cnt0  21198  ist1-3  21201  ishaus2  21203  cmpfi  21259  dfconn2  21270  1stccnp  21313  1stccn  21314  subislly  21332  hausmapdom  21351  kgencn  21407  tx1cn  21460  tx2cn  21461  txcnmpt  21475  txrest  21482  hauseqlcld  21497  tgqtop  21563  qtopcld  21564  qtopcn  21565  ordthmeolem  21652  trfil2  21738  trfil3  21739  trnei  21743  ufildr  21782  fmfg  21800  rnelfm  21804  fmfnfm  21809  elflim  21822  fbflim  21827  flimrest  21834  isflf  21844  cnflf  21853  cnflf2  21854  fclscf  21876  cnfcf  21893  ptcmplem2  21904  ghmcnp  21965  tsmssubm  21993  iscfilu  22139  xmetgt0  22210  prdsxmetlem  22220  elbl2ps  22241  elbl2  22242  blcomps  22245  blcom  22246  xblpnfps  22247  xblpnf  22248  blpnf  22249  xmeter  22285  setsxms  22331  imasf1obl  22340  stdbdbl  22369  metrest  22376  metcn  22395  txmetcn  22400  metuel2  22417  dscopn  22425  xrtgioo  22656  metdstri  22701  cncffvrn  22748  cnmpt2pc  22774  iihalf2  22779  icopnfhmeo  22789  evth2  22806  lmmbr3  23104  iscau3  23122  lmclimf  23148  metcld  23150  cfilucfil3  23163  srabn  23202  rrxmet  23237  minveclem4  23249  evthicc2  23275  ovolfioo  23282  ovolficc  23283  ovolgelb  23294  ovoliun  23319  shft2rab  23322  ovolshftlem1  23323  sca2rab  23326  ovolscalem1  23327  ismbl2  23341  ioombl1lem4  23375  mbfmulc2lem  23459  mbfmax  23461  mbfposr  23464  ismbf3d  23466  mbfaddlem  23472  mbfsup  23476  mbfinf  23477  i1f1lem  23501  i1fmulclem  23514  mbfi1fseqlem4  23530  itg2seq  23554  itg2monolem1  23562  itg2cnlem1  23573  itgfsum  23638  ditgneg  23666  limcdif  23685  limcnlp  23687  cnplimc  23696  rolle  23798  mvth  23800  dvne0  23819  lhop1lem  23821  itgsubst  23857  mdegle0  23882  deg1leb  23900  deg1le0  23916  q1peqb  23959  coemulhi  24055  dgrlt  24067  plydivlem3  24095  vieta1lem2  24111  aannenlem1  24128  ulmres  24187  reefiso  24247  pilem3  24252  ellogdm  24430  root1eq1  24541  angpieqvdlem  24600  angpieqvdlem2  24601  quad2  24611  1cubr  24614  quart  24633  rlimcnp  24737  wilthlem2  24840  isppw  24885  dvdsflsumcom  24959  fsumvma  24983  logfac2  24987  chpchtsum  24989  dchrmulcl  25019  dchreq  25028  dchrresb  25029  bclbnd  25050  bposlem1  25054  bposlem5  25058  lgsneg  25091  gausslemma2dlem0c  25128  lgsquadlem1  25150  lgsquadlem2  25151  m1lgs  25158  2lgsoddprmlem2  25179  dchrisumlem3  25225  dchrisum0lem1  25250  trgcgrg  25455  tgellng  25493  lnrot1  25563  islnopp  25676  ismidb  25715  islmib  25724  isleag  25778  ttgelitv  25808  axsegconlem6  25847  axeuclidlem  25887  axcontlem2  25890  axcontlem4  25892  axcontlem12  25900  ausgrusgrb  26105  nb3grpr2  26329  cplgr2v  26384  umgr2v2enb1  26478  crctcsh  26772  wspthsnwspthsnonOLD  26881  dfconngr1  27166  eupth2lems  27216  nmoreltpnf  27752  isblo2  27766  nmlnogt0  27780  phoeqi  27841  ubthlem2  27855  hire  28079  normgt0  28112  ho01i  28815  ho02i  28816  hoeq1  28817  hoeq2  28818  nmopreltpnf  28856  adjeq  28922  leop  29110  leopmul2i  29122  pjnormssi  29155  pjimai  29163  jplem1  29255  mddmd2  29296  mdslmd1lem1  29312  mdslmd1lem2  29313  superpos  29341  atnssm0  29363  dmdbr5ati  29409  disjunsn  29533  fcoinvbr  29545  ofpreima  29593  funcnv5mpt  29597  isoun  29607  fpwrelmapffslem  29635  fpwrelmap  29636  iocinioc2  29669  xrdifh  29670  nndiffz1  29676  xdivmul  29761  isarchi2  29867  smatrcl  29990  fimaproj  30028  sqsscirc2  30083  xrmulc1cn  30104  ismntoplly  30197  esumfsup  30260  1stmbfm  30450  2ndmbfm  30451  mbfmcnt  30458  eulerpartlems  30550  eulerpartlemd  30556  ballotlemfc0  30682  ballotlemfcc  30683  ballotlemsima  30705  ballotlemfrcn0  30719  sgn3da  30731  reprinfz1  30828  reprdifc  30833  bnj1173  31196  erdszelem7  31305  erdszelem9  31307  iscvm  31367  cvmlift3lem4  31430  sltval2  31934  noextenddif  31946  sleloe  32004  sletri3  32005  fscgr  32312  seglelin  32348  btwnoutside  32357  lineunray  32379  cldbnd  32446  isfne4  32460  fneval  32472  filnetlem4  32501  nndivsub  32581  dfgcd3  33300  wl-sbhbt  33465  wl-sbcom2d  33474  wl-sbalnae  33475  wl-ax11-lem8  33499  sin2h  33529  cos2h  33530  matunitlindflem1  33535  matunitlindflem2  33536  matunitlindf  33537  ptrest  33538  poimirlem3  33542  poimirlem4  33543  poimirlem22  33561  poimirlem27  33566  mblfinlem3  33578  mblfinlem4  33579  ismblfin  33580  itg2addnclem  33591  itg2addnclem2  33592  itg2gt0cn  33595  iblabsnclem  33603  ftc1anclem6  33620  areacirclem2  33631  areacirclem5  33634  areacirc  33635  cover2  33638  mettrifi  33683  drngoi  33880  eldm4  34178  exanres2  34206  brcoss2  34327  br1cossres2  34335  eldmcoss2  34349  eldm1cossres2  34351  brcosscnv2  34363  prter3  34486  islshpat  34622  lsatnle  34649  ellkr2  34696  lshpkr  34722  lkr0f2  34766  lduallkr3  34767  lkreqN  34775  cvrval2  34879  isat3  34912  glbconN  34981  hlrelat5N  35005  cvrval4N  35018  atlt  35041  1cvrco  35076  pmaple  35365  isline2  35378  isline4N  35381  elpaddn0  35404  elpadd2at2  35411  cdlemkid4  36539  dia0  36658  cdlemm10N  36724  dibglbN  36772  dihmeetlem4preN  36912  dochkrshp3  36994  dvh4dimlem  37049  lcfl5  37102  mapdpglem3  37281  mapdheq  37334  hdmap1eq  37408  hdmapval2lem  37440  hdmapoc  37540  hlhillcs  37567  fz1eqin  37649  diophin  37653  jm2.19  37877  rmxdiophlem  37899  pw2f1ocnv  37921  wepwsolem  37929  gicabl  37986  sdrgacs  38088  idomodle  38091  isdomn3  38099  ntrclsfveq2  38676  ntrclsss  38678  ntrclsk4  38687  extoimad  38781  radcnvrat  38830  bcc0  38856  unima  39660  supxrre3rnmpt  39969  clim2f  40186  clim2f2  40220  liminfreuzlem  40352  liminfltlem  40354  2reu4a  41510  dfdfat2  41532  funbrafv2b  41560  dfafn5a  41561  leaddsuble  41636  iccpartgtprec  41681  pfxsuffeqwrdeq  41731  flsqrt  41833  dfeven2  41887  dfodd3  41888  lindslinindimp2lem4  42575  snlindsntor  42585  regt1loggt0  42655  elbigo2  42671  elbigolo1  42676  fldivexpfllog2  42684  nnlog2ge0lt1  42685  blenpw2m1  42698
  Copyright terms: Public domain W3C validator