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

Theorem jaoi 851
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 845 . . 3 ((𝜑𝜒) → (¬ 𝜑𝜒))
2 jaoi.2 . . 3 (𝜒𝜓)
31, 2syl6 35 . 2 ((𝜑𝜒) → (¬ 𝜑𝜓))
4 jaoi.1 . 2 (𝜑𝜓)
53, 4pm2.61d2 182 1 ((𝜑𝜒) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 841
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  df-or 842
This theorem is referenced by:  jao1i  852  jaod  853  pm1.4  863  pm3.2ni  874  pm1.2  897  pm2.4  900  pm2.41  901  orim12i  902  pm1.5  913  pm2.42  936  jaoa  949  jaoian  950  pm4.44  990  andi  1001  ecase3  1024  cases2ALT  1040  consensus  1044  jaoi3  1052  1fpid3  1071  19.33  1876  19.33b  1877  nfim1  2189  dfsb2  2525  dfsb2ALT  2584  mooran1  2632  2eu3OLD  2733  eueq3  3699  sbcor  3819  sspss  4073  sspsstr  4079  elun  4122  ssun  4162  inss  4212  raaan2  4460  ifbi  4484  ifcomnan  4517  elpr2  4581  rabsnifsb  4650  tpprceq3  4729  tppreqb  4730  pwpw0  4738  sssn  4751  snsssn  4764  preq12b  4773  prnebg  4778  preq12nebg  4785  elpr2elpr  4791  pwsnALT  4823  prproe  4828  3elpr2eq  4829  unissint  4891  zfpair  5312  propeqop  5388  propssopi  5389  opthhausdorff  5398  opthhausdorff0  5399  iunopeqop  5402  relsnb  5668  iresn0n0  5916  sotri2  5982  sotri3  5983  somincom  5987  ordssun  6283  onun2i  6299  unizlim  6300  onxpdisj  6303  tpres  6955  sorpssuni  7447  ordeleqon  7492  ordunisuc  7536  orduninsuc  7547  tfinds  7563  limomss  7574  limom  7584  soxp  7812  ressuppssdif  7840  tfr2b  8021  omopthi  8273  domnsym  8631  brwdom  9019  cantnfvalf  9116  djuss  9337  djuunxp  9338  eldju2ndl  9341  eldju2ndr  9342  djuun  9343  updjud  9351  iscard3  9507  cflim2  9673  sornom  9687  isfin5  9709  isfin6  9710  sdom2en01  9712  fin23lem29  9751  fin23lem30  9752  fin56  9803  fin67  9805  hsmexlem9  9835  axcc4dom  9851  axdc3lem2  9861  axdc3lem4  9863  brdom3  9938  winainflem  10103  r1tskina  10192  indpi  10317  ltxrlt  10699  nn0sub  11935  nn0n0n1ge2b  11951  nn0ge2m1nn  11952  xnn0xr  11960  xnn0nemnf  11966  elnn0z  11982  nn0lt10b  12032  nn0le2is012  12034  nn0ind-raph  12070  uzin  12266  indstr2  12315  nn0ledivnn  12490  xrnemnf  12500  xrnepnf  12501  mnfltxr  12510  xnn0n0n1ge2b  12514  xnn0ge0  12516  xnn0xaddcl  12616  xnn0lenn0nn0  12626  xnn0xadd0  12628  xmullem2  12646  rexmul  12652  xnn0xrge0  12879  elfzonlteqm1  13101  elfznelfzo  13130  injresinjlem  13145  injresinj  13146  fldiv4p1lem1div2  13193  fldiv4lem1div2  13195  modfzo0difsn  13299  ssnn0fi  13341  fsuppmapnn0fiubex  13348  m1expcl2  13439  m1expeven  13464  sq01  13574  expnngt1  13590  nn0opthi  13618  facp1  13626  faclbnd3  13640  faclbnd4lem1  13641  faclbnd4lem3  13643  bcn1  13661  hashnemnf  13692  hashv01gt1  13693  hashneq0  13713  hashrabrsn  13721  hashrabsn01  13722  hashrabsn1  13723  hashunx  13735  hashsnle1  13766  hashfzp1  13780  hash2pwpr  13822  hashge2el2difr  13827  swrdnd2  14005  pfxnd0  14038  repswswrd  14134  relexpsucr  14376  relexpsucl  14380  relexpcnv  14382  relexprelg  14385  relexpdmg  14389  relexprng  14393  relexpfld  14396  relexpaddg  14400  sumz  15067  arisum  15203  arisum2  15204  pwdif  15211  ntrivcvg  15241  prod1  15286  fprodfac  15315  mod2eq1n2dvds  15684  mulsucdiv2z  15690  nn0o1gt2  15720  nno  15721  nn0o  15722  sumeven  15726  sumodd  15727  divalglem1  15733  divalglem6  15737  gcdaddmlem  15860  dfgcd2  15882  mulgcd  15884  lcmf  15965  lcmfunsnlem2lem2  15971  lcmfunsnlem2  15972  prm2orodd  16023  dfphi2  16099  nnnn0modprm0  16131  prm23lt5  16139  oddprmdvds  16227  4sqlem19  16287  ramz  16349  prmolefac  16370  prmgaplem7  16381  cshwshashlem1  16417  ressval3d  16549  firest  16694  xpsfeq  16824  funcres2c  17159  mulgnn0gsum  18172  symgfix2  18473  pmtrprfval  18544  m1expaddsub  18555  psgnprfval  18578  gsumpr  19004  gsumzunsnd  19005  sralem  19878  0ringnnzr  19970  frgpcyg  20648  cnmsgnsubg  20649  psgninv  20654  zrhpsgnelbas  20666  m2detleiblem1  21161  symgmatr01lem  21190  indiscld  21627  pnfnei  21756  mnfnei  21757  alexsubALTlem2  22584  alexsubALTlem3  22585  dscmet  23109  xrtgioo  23341  ishl2  23900  iunmbl2  24085  icombl  24092  ioombl  24093  recnprss  24429  recnperf  24430  dvexp2  24478  dvexp3  24502  dvne0f1  24536  plypf1  24729  taylfvallem1  24872  taylfval  24874  tayl0  24877  coseq0negpitopi  25016  logfac  25111  cxpexp  25178  pythag  25322  reasinsin  25401  harmonicbnd3  25512  lgslem4  25803  gausslemma2dlem0i  25867  lgsquadlem2  25884  2lgslem3  25907  2lgs  25910  2lgsoddprmlem3  25917  2sqnn0  25941  2sqnn  25942  cchhllem  26600  lfgrnloop  26837  uhgr2edg  26917  usgredg4  26926  usgredg2v  26936  usgrexmplef  26968  nb3grprlem1  27089  uvtx01vtx  27106  wlk1walk  27347  upgriswlk  27349  pthdadjvtx  27438  upgrwlkdvdelem  27444  pthdlem2lem  27475  2pthon3v  27649  clwwlkn  27731  clwwlkneq0  27734  eupth2lem3lem4  27937  konigsberg  27963  3vfriswmgrlem  27983  1to2vfriswmgr  27985  1to3vfriswmgr  27986  frgrregorufr0  28030  numclwlk1  28077  ex-pr  28136  shunssi  29072  cvmdi  30028  1neg1t1neg1  30399  iundisj2cnt  30448  fz1nnct  30452  xrge0iifiso  31077  esumpr2  31225  measiuns  31375  sxbrsigalem0  31428  bnj964  32114  subfacval3  32333  kur14lem7  32356  satfrnmapom  32514  gonar  32539  goalr  32541  mrsubcv  32654  nepss  32845  fz0n  32859  bccolsum  32868  dfon2lem7  32931  trpredlem1  32963  trpred0  32972  sltres  33066  nolesgn2o  33075  nosep1o  33083  altopthsn  33319  elhf2  33533  nn0prpw  33568  dissym1  33666  ordcmp  33692  bj-currypeirce  33789  bj-jaoi1  33801  bj-jaoi2  33802  bj-ififc  33812  bj-andnotim  33819  bj-nfimexal  33856  bj-sbsb  34057  bj-elsn12g  34247  bj-ideqg1  34348  finxpreclem2  34553  wl-equsal1i  34664  tan2h  34765  poimirlem23  34796  poimirlem32  34805  itg2addnclem  34824  orfa1  35244  orfa2  35245  imaexALTV  35468  inex3  35476  inxpex  35477  elpadd0  36825  sbor2  38982  sn-0ne2  39114  sn-0lt1  39124  hbtlem5  39606  rp-fakeimass  39756  rp-isfinite6  39762  pr2cv  39785  iunrelexp0  39925  relexpss1d  39928  relexpmulg  39933  iunrelexpmin2  39935  relexp01min  39936  relexp0a  39939  relexpxpmin  39940  relexpaddss  39941  clsk1indlem3  40271  ssrecnpr  40517  seff  40518  sblpnf  40519  expgrowthi  40542  dvconstbi  40543  19.33-2  40591  ax6e2ndeq  40770  en3lpVD  41056  undif3VD  41093  ax6e2ndeqVD  41120  ax6e2ndeqALT  41142  iooinlbub  41652  elprneb  43141  euoreqb  43185  2reu3  43186  afvpcfv0  43222  afvfv0bi  43228  afvco2  43252  afv2orxorb  43304  afv2ndeffv0  43336  afv2fv0b  43342  fvmptrabdm  43369  iccpartltu  43462  iccpartgtl  43463  iccpartgt  43464  iccpartleu  43465  iccpartgel  43466  iccpartnel  43475  elsprel  43514  prsprel  43526  sprsymrelfolem2  43532  paireqne  43550  odz2prm2pw  43602  fmtnofac1  43609  fmtno4prmfac  43611  31prm  43637  lighneallem2  43648  lighneallem3  43649  lighneallem4b  43651  lighneallem4  43652  zeo2ALTV  43713  nn0o1gt2ALTV  43736  nn0oALTV  43738  stgoldbwt  43818  sbgoldbwt  43819  sbgoldbalt  43823  sbgoldbm  43826  sbgoldbo  43829  nnsum3primesle9  43836  nnsum4primeseven  43842  nnsum4primesevenALTV  43843  wtgoldbnnsum4prm  43844  bgoldbnnsum3prm  43846  bgoldbtbndlem1  43847  bgoldbtbnd  43851  tgoldbach  43859  isomuspgrlem1  43869  upgrwlkupwlk  43892  smndex1basss  44005  smndex1mgm  44007  smndex1mndlem  44009  ztprmneprm  44323  islinindfis  44432  lindslinindsimp2lem5  44445  lindslinindsimp2  44446  lindsrng01  44451  elfzolborelfzop1  44502  flnn0div2ge  44521  blennn0elnn  44565  blen1b  44576  nnolog2flm1  44578  blengt1fldiv2p1  44581  0dig2pr01  44598  dignn0flhalf  44606  nn0sumshdiglemB  44608  nn0sumshdiglem1  44609  resum2sqorgt0  44624  rrx2xpref1o  44633  rrx2plord2  44637  itsclc0yqsol  44679
  Copyright terms: Public domain W3C validator