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

Theorem bitr4d 283
Description: Deduction form of bitr4i 279. (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 224 . 2 (𝜑 → (𝜒𝜃))
41, 3bitrd 280 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207
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 208
This theorem is referenced by:  3bitr2d  308  3bitr2rd  309  3bitr4d  312  3bitr4rd  313  bianabs  542  mpbirand  703  sb3b  2497  sbcom3  2544  sbal1  2568  sbal2  2569  sbal2OLD  2570  2reu4lem  4463  issn  4757  disjprgw  5053  disjprg  5054  reuhypd  5311  ordtri3  6221  ordsssuc  6271  iota1  6326  funbrfv2b  6717  dffn5  6718  feqmptdf  6729  unima  6733  dmfco  6751  fneqeql  6809  f1ompt  6868  dff13  7004  fliftcnv  7053  soisores  7069  isotr  7078  isoini  7080  caovord3  7350  releldm2  7733  fimaproj  7820  brtpos  7892  tpostpos  7903  oe1m  8161  oawordri  8166  oalimcl  8176  omlimcl  8194  omabs  8264  iserd  8305  qliftel  8370  qliftfun  8372  qliftf  8375  ecopovsym  8389  pw2f1olem  8610  mapen  8670  suppeqfsuppbi  8836  mapfien  8860  supisolem  8926  cantnflem1  9141  wemapwe  9149  rankr1clem  9238  rankr1c  9239  ranklim  9262  r1pwALT  9264  r1pwcl  9265  isfin1-2  9796  isfin1-4  9798  fin71num  9808  axdc3lem2  9862  ltmnq  10383  prlem936  10458  ltsosr  10505  ltasr  10511  xrlenlt  10695  ltxrlt  10700  letri3  10715  ne0gt0  10734  subadd  10878  ltsubadd2  11100  lesubadd2  11102  suble  11107  ltsub23  11109  ltaddpos2  11120  ltsubpos  11121  subge02  11145  ltord2  11158  leord2  11159  ltaddsublt  11256  divmul  11290  divmul3  11292  rec11r  11328  ltdiv1  11493  ltdivmul2  11506  ledivmul2  11508  ltrec  11511  ltdiv2  11515  negfi  11578  negiso  11610  nnle1eq1  11656  avgle1  11866  avgle2  11867  avgle  11868  nn0le0eq0  11914  elz2  11988  znnnlt1  11998  zleltp1  12022  difrp  12417  xrltlen  12529  dfle2  12530  xrletri3  12537  xgepnf  12548  xlemnf  12550  qbtwnre  12582  xltnegi  12599  supxrre  12710  infxrre  12719  elioo5  12784  elfz5  12890  elfzm11  12968  predfz  13022  flbi  13176  flbi2  13177  fldiv4lem1div2uz2  13196  fznnfl  13220  zmodid2  13257  2submod  13290  lt2sq  13488  le2sq  13489  sqlecan  13561  bcval5  13668  pfxsuffeqwrdeq  14050  shftfib  14421  mulre  14470  cnpart  14589  sqrlem6  14597  sqrmo  14601  elicc4abs  14669  abs2difabs  14684  cau4  14706  limsupgre  14828  clim2  14851  ello1mpt2  14869  lo1resb  14911  o1resb  14913  climeq  14914  climmpt2  14920  isercoll  15014  caucvgb  15026  fsumabs  15146  isumshft  15184  geomulcvg  15222  absefib  15541  dvdsval3  15601  dvdsabseq  15653  dvdsflip  15657  dvdsssfz1  15658  mod2eq1n2dvds  15686  ndvdsadd  15751  bitscmp  15777  smupvallem  15822  dvdssq  15901  lcmdvds  15942  ncoprmgcdgt1b  15985  isprm3  16017  isprm5  16041  phiprmpw  16103  prmdiv  16112  pc11  16206  pcz  16207  pockthlem  16231  prmreclem2  16243  prmreclem4  16245  prmreclem6  16247  1arith  16253  vdwapun  16300  rami  16341  ramcl  16355  pwsle  16755  ercpbllem  16811  invsym  17022  funcres2c  17161  latnle  17685  grpinvcnv  18107  subgacs  18253  eqger  18270  gexdvds2  18641  pgpfi1  18651  pgpfi  18661  lsmass  18726  lssnle  18731  lsmdisj3b  18747  lsmhash  18762  ablsubadd  18863  gsumval3lem2  18957  subgdmdprd  19087  pgpfac1lem2  19128  dvdsr02  19337  drngid2  19449  issubrg3  19494  sdrgacs  19511  lssacs  19670  psrbaglefi  20082  coe1mul2lem1  20365  prmirred  20572  chrdvds  20605  chrcong  20606  chrnzr  20607  znleval  20631  znleval2  20632  cygznlem3  20646  frlmbas  20829  elfilspd  20877  lindfmm  20901  islindf4  20912  islindf5  20913  mdetunilem9  21159  isneip  21643  neiptopnei  21670  lpdifsn  21681  restopnb  21713  restopn2  21715  restdis  21716  restperf  21722  lmbr2  21797  cncls2  21811  cnprest  21827  cnprest2  21828  iscnrm2  21876  ist0-2  21882  ist1-3  21887  ishaus2  21889  cmpfi  21946  dfconn2  21957  1stccnp  22000  subislly  22019  hausmapdom  22038  tx1cn  22147  tx2cn  22148  txcnmpt  22162  txrest  22169  hauseqlcld  22184  tgqtop  22250  qtopcld  22251  ordthmeolem  22339  trfil2  22425  trfil3  22426  trnei  22430  ufildr  22469  fmfg  22487  rnelfm  22491  fmfnfm  22496  elflim  22509  flimrest  22521  cnflf  22540  cnflf2  22541  ptcmplem2  22591  ghmcnp  22652  tsmssubm  22680  iscfilu  22826  xmetgt0  22897  prdsxmetlem  22907  blcomps  22932  blcom  22933  xblpnfps  22934  xblpnf  22935  blpnf  22936  xmeter  22972  setsxms  23018  imasf1obl  23027  stdbdbl  23056  metrest  23063  metuel2  23104  dscopn  23112  xrtgioo  23343  metdstri  23388  cnmpopc  23461  iihalf2  23466  icopnfhmeo  23476  evth2  23493  lmmbr3  23792  iscau3  23810  metcld  23838  cfilucfil3  23852  srabn  23892  rrxmet  23940  minveclem4  23964  evthicc2  23990  ovolgelb  24010  shft2rab  24038  ovolshftlem1  24039  sca2rab  24042  ovolscalem1  24043  ioombl1lem4  24091  mbfmulc2lem  24177  ismbf3d  24184  mbfsup  24194  mbfinf  24195  i1f1lem  24219  i1fmulclem  24232  mbfi1fseqlem4  24248  itg2seq  24272  ditgneg  24384  limcdif  24403  limcnlp  24405  cnplimc  24414  rolle  24516  mvth  24518  dvne0  24537  lhop1lem  24539  itgsubst  24575  mdegle0  24600  deg1leb  24618  deg1le0  24634  q1peqb  24677  coemulhi  24773  dgrlt  24785  plydivlem3  24813  vieta1lem2  24829  aannenlem1  24846  ulmres  24905  reefiso  24965  pilem3  24970  ellogdm  25149  root1eq1  25263  angpieqvdlem  25333  angpieqvdlem2  25334  quad2  25344  1cubr  25347  quart  25366  rlimcnp  25471  wilthlem2  25574  isppw  25619  dvdsflsumcom  25693  fsumvma  25717  logfac2  25721  chpchtsum  25723  dchrmulcl  25753  dchrresb  25763  bclbnd  25784  bposlem1  25788  bposlem5  25792  gausslemma2dlem0c  25862  lgsquadlem1  25884  m1lgs  25892  2lgsoddprmlem2  25913  dchrisumlem3  25995  dchrisum0lem1  26020  tgjustr  26188  trgcgrg  26229  lnrot1  26337  islnopp  26453  ismidb  26492  islmib  26501  axsegconlem6  26636  axeuclidlem  26676  axcontlem2  26679  axcontlem4  26681  axcontlem12  26689  ausgrusgrb  26878  nb3grpr2  27093  cplgr2v  27142  umgr2v2enb1  27236  crctcsh  27530  clwwlknonwwlknonb  27813  eupth2lems  27945  nmoreltpnf  28474  isblo2  28488  nmlnogt0  28502  phoeqi  28562  ubthlem2  28576  hire  28799  normgt0  28832  ho01i  29533  ho02i  29534  hoeq1  29535  hoeq2  29536  nmopreltpnf  29574  adjeq  29640  leop  29828  leopmul2i  29840  pjnormssi  29873  pjimai  29881  jplem1  29973  mddmd2  30014  mdslmd1lem1  30030  mdslmd1lem2  30031  superpos  30059  atnssm0  30081  dmdbr5ati  30127  disjunsn  30273  fcoinvbr  30287  ofpreima  30339  funcnv5mpt  30342  isoun  30364  fpwrelmapffslem  30395  fpwrelmap  30396  iocinioc2  30429  xrdifh  30430  nndiffz1  30436  xdivmul  30529  cntzsnid  30624  isarchi2  30742  finexttrb  30952  smatrcl  30961  sqsscirc2  31052  xrmulc1cn  31073  esumfsup  31229  1stmbfm  31418  2ndmbfm  31419  mbfmcnt  31426  eulerpartlems  31518  eulerpartlemd  31524  ballotlemfc0  31650  ballotlemfcc  31651  ballotlemsima  31673  ballotlemfrcn0  31687  sgn3da  31699  reprinfz1  31793  reprdifc  31798  bnj1173  32172  zltp1ne  32246  lfuhgr2  32263  erdszelem7  32342  erdszelem9  32344  iscvm  32404  cvmlift3lem4  32467  sltval2  33061  noextenddif  33073  sleloe  33131  sletri3  33132  fscgr  33439  seglelin  33475  btwnoutside  33484  lineunray  33506  cldbnd  33572  isfne4  33586  fneval  33598  filnetlem4  33627  nndivsub  33703  dfgcd3  34488  fvineqsneu  34575  wl-sbhbt  34672  wl-sbcom2d  34679  wl-sbalnae  34680  wl-ax11-lem8  34706  wl-dfrmof  34737  sin2h  34764  cos2h  34765  matunitlindflem1  34770  matunitlindflem2  34771  matunitlindf  34772  ptrest  34773  poimirlem3  34777  poimirlem4  34778  poimirlem22  34796  poimirlem27  34801  mblfinlem3  34813  mblfinlem4  34814  ismblfin  34815  itg2addnclem  34825  itg2addnclem2  34826  itg2gt0cn  34829  iblabsnclem  34837  ftc1anclem6  34854  areacirclem2  34865  areacirclem5  34868  areacirc  34869  mettrifi  34915  drngoi  35112  eldm4  35414  exanres2  35437  brcoss2  35559  br1cossres2  35567  eldmcoss2  35581  eldm1cossres2  35583  brcosscnv2  35595  erim2  35793  prter3  35900  islshpat  36035  lsatnle  36062  ellkr2  36109  lshpkr  36135  lkr0f2  36179  lduallkr3  36180  lkreqN  36188  cvrval2  36292  isat3  36325  glbconN  36395  hlrelat5N  36419  cvrval4N  36432  atlt  36455  1cvrco  36490  pmaple  36779  isline2  36792  isline4N  36795  elpaddn0  36818  elpadd2at2  36825  cdlemkid4  37952  dia0  38070  cdlemm10N  38136  dibglbN  38184  dihmeetlem4preN  38324  dochkrshp3  38406  dvh4dimlem  38461  lcfl5  38514  mapdpglem3  38693  mapdheq  38746  hdmap1eq  38819  hdmapval2lem  38849  hdmapoc  38949  hlhillcs  38976  renegadd  39082  resubadd  39089  fz1eqin  39246  diophin  39249  jm2.19  39470  rmxdiophlem  39492  pw2f1ocnv  39514  wepwsolem  39522  gicabl  39579  idomodle  39676  isdomn3  39684  ntrclsfveq2  40291  ntrclsss  40293  ntrclsk4  40302  extoimad  40395  radcnvrat  40526  bcc0  40552  supxrre3rnmpt  41583  clim2f  41797  clim2f2  41831  liminfreuzlem  41963  liminfltlem  41965  xlimmnflimsup2  42013  xlimpnfliminf2  42022  xlimlimsupleliminf  42024  opprb  43147  funbrafv2b  43239  dfafn5a  43240  leaddsuble  43378  iccpartgtprec  43427  flsqrt  43603  dfeven2  43661  dfodd3  43662  lindslinindimp2lem4  44414  snlindsntor  44424  regt1loggt0  44494  elbigo2  44510  elbigolo1  44515  fldivexpfllog2  44523  nnlog2ge0lt1  44524  blenpw2m1  44537
  Copyright terms: Public domain W3C validator