MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  jaoi Unicode version

Theorem jaoi 379
Description: Inference disjoining the antecedents of two implications. (Contributed by NM, 5-Apr-1994.)
Hypotheses
Ref Expression
jaoi.1
jaoi.2
Assertion
Ref Expression
jaoi

Proof of Theorem jaoi
StepHypRef Expression
1 pm2.53 373 . . 3
2 jaoi.2 . . 3
31, 2syl6 33 . 2
4 jaoi.1 . 2
53, 4pm2.61d2 160 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  \/wo 368
This theorem is referenced by:  jaod  380  pm1.4  386  jaoa  510  pm1.2  513  orim12i  516  pm1.5  522  pm2.41  573  pm2.42  574  pm2.4  575  pm4.44  577  jaoian  784  pm2.64  789  pm2.82  852  pm3.2ni  854  andi  867  ecase3  941  consensus  959  jaoi3  969  cases2  971  cad1  1465  19.33  1695  19.33b  1696  19.40b  1698  dfsb2  2114  mooran1  2348  2eu3  2379  eueq3  3274  sbcor  3372  sspss  3602  sspsstr  3608  elun  3644  ssun  3682  inss  3726  undif3  3758  ifbi  3962  ifcomnan  3990  elpr2  4048  rabsnifsb  4098  tpprceq3  4170  tppreqb  4171  pwpw0  4178  sssn  4188  snsssn  4198  preq12b  4206  prnebg  4212  pwsnALT  4244  unissint  4311  reusv6OLD  4663  reusv7OLD  4664  zfpair  4689  ordelinel  4981  ordssun  4982  ordequn  4983  onun2i  4998  unizlim  4999  onxpdisj  5088  sotri2  5401  sotri3  5402  somincom  5409  funtpg  5643  fvfundmfvn0  5903  sorpssuni  6589  sorpssint  6590  ordeleqon  6624  ordunisuc  6667  orduninsuc  6678  tfinds  6694  limomss  6705  limom  6715  soxp  6913  ressuppssdif  6940  tfr2b  7084  omopthi  7325  domnsym  7663  brwdom  8014  cantnfvalf  8105  iscard3  8495  cflim2  8664  sornom  8678  isfin5  8700  isfin6  8701  sdom2en01  8703  fin23lem29  8742  fin23lem30  8743  fin56  8794  fin67  8796  hsmexlem9  8826  axcc4dom  8842  axdc3lem2  8852  axdc3lem4  8854  brdom3  8927  winainflem  9092  r1tskina  9181  indpi  9306  ltxrlt  9676  ltlen  9707  elnnnn0b  10865  nn0sub  10871  nn0n0n1ge2b  10885  nn0ge2m1nn  10886  elnn0z  10902  nn0lt10b  10950  nn0ind-raph  10989  uzin  11142  indstr2  11189  xrnemnf  11357  xrnepnf  11358  mnfltxr  11365  nn0pnfge0  11370  xmullem2  11486  rexmul  11492  elfzonlteqm1  11891  elfznelfzo  11915  injresinjlem  11925  injresinj  11926  ssnn0fi  12094  fsuppmapnn0fiubex  12098  m1expcl2  12188  sq01  12288  nn0opthi  12350  facp1  12358  faclbnd3  12370  faclbnd4lem1  12371  faclbnd4lem3  12373  bcn1  12391  hashnemnf  12417  hashv01gt1  12418  hashneq0  12434  hashrabrsn  12440  hashrabsn01  12441  hashrabsn1  12442  hashunx  12454  hash2pwpr  12519  swrdnd  12657  swrdvalodm2  12664  swrdvalodm  12665  repswswrd  12756  scshwfzeqfzo  12794  sumz  13544  arisum  13671  arisum2  13672  ntrivcvg  13706  prod1  13751  fprodfac  13777  divalglem1  14052  divalglem6  14056  gcdaddmlem  14166  mulgcd  14184  dfphi2  14304  nnnn0modprm0  14331  4sqlem19  14481  ramz  14543  cshwshashlem1  14580  firest  14830  xpsfeq  14961  xpsfrnel2  14962  funcres2c  15270  symgfix2  16441  pmtrprfval  16512  m1expaddsub  16523  psgnprfval  16546  gsumzunsnd  16982  sralem  17823  0ringnnzr  17917  prmirred  18525  prmirredOLD  18528  frgpcyg  18612  cnmsgnsubg  18613  psgninv  18618  zrhpsgnelbas  18630  m2detleiblem1  19126  symgmatr01lem  19155  pmatcollpw3fi1  19289  indiscld  19592  pnfnei  19721  mnfnei  19722  alexsubALTlem2  20548  alexsubALTlem3  20549  dscmet  21093  xrtgioo  21311  ishl2  21810  iunmbl2  21967  icombl  21974  ioombl  21975  recnprss  22308  recnperf  22309  dvexp2  22357  dvexp3  22379  dvne0f1  22413  plypf1  22609  taylfvallem1  22752  taylfval  22754  tayl0  22757  coseq0negpitopi  22896  logfac  22985  cxpexp  23049  pythag  23149  reasinsin  23227  harmonicbnd3  23337  lgslem4  23574  lgsquadlem2  23630  cchhllem  24190  usgraedgprv  24376  usgraedgrnv  24377  usgraedg4  24387  usgraidx2v  24393  usgraexmpl  24401  nb3graprlem1  24451  wlkdvspthlem  24609  usgra2adedgspthlem2  24612  usgra2wlkspthlem1  24619  constr3trllem2  24651  clwwlkgt0  24771  clwwlknprop  24772  vdgrf  24898  rusgrasn  24945  clwlknclwlkdifs  24960  konigsberg  24987  3vfriswmgralem  25004  1to2vfriswmgra  25006  1to3vfriswmgra  25007  vdgfrgragt2  25027  frgrawopreglem2  25045  frgrawopreglem3  25046  frgraregorufr0  25052  ex-pr  25151  shunssi  26286  cvmdi  27243  iundisj2cnt  27604  xrge0iifiso  27917  esumpr2  28074  measiuns  28188  sxbrsigalem0  28242  subfacval3  28633  kur14lem7  28656  m1expevenALT  28663  mrsubcv  28870  nepss  29095  fz0n  29110  dfon2lem7  29221  trpredlem1  29310  trpred0  29319  sltres  29424  altopthsn  29611  elhf2  29832  dissym1  29886  ordcmp  29912  wl-equsal1i  29996  tan2h  30047  itg2addnclem  30066  nn0prpw  30141  orfa1  30484  orfa2  30485  prtlem1  30584  hbtlem5  31077  ssrecnpr  31188  seff  31189  sblpnf  31190  expgrowthi  31238  dvconstbi  31239  19.33-2  31287  znnn0nn  31489  iooinlbub  31534  raaan2  32180  2reu3  32193  afvpcfv0  32231  afvfv0bi  32237  afvco2  32261  usgvincvad  32404  usgvincvadALT  32407  usgedgvadf1  32415  usgedgvadf1ALT  32418  tpres  32554  ressval3d  32558  ztprmneprm  32936  gsumpr  32950  nn0le2is012  32956  islinindfis  33050  lindslinindsimp2lem5  33063  lindslinindsimp2  33064  lindsrng01  33069  ax6e2ndeq  33332  en3lpVD  33645  undif3VD  33682  ax6e2ndeqVD  33709  ax6e2ndeqALT  33731  bnj964  34001  bj-jaoi1  34148  bj-jaoi2  34149  bj-andnotim  34177  elpadd0  35533  rp-fakeimass  37736  rp-isfinite6  37744
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 185  df-or 370
  Copyright terms: Public domain W3C validator