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

Theorem jaoi 853
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 847 . . 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 843
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 844
This theorem is referenced by:  jao1i  854  jaod  855  pm1.4  865  pm3.2ni  876  pm1.2  899  pm2.4  902  pm2.41  903  orim12i  904  pm1.5  915  pm2.42  938  jaoa  951  jaoian  952  pm4.44  992  andi  1003  ecase3  1026  cases2ALT  1042  consensus  1046  jaoi3  1054  1fpid3  1073  19.33  1878  19.33b  1879  nfim1  2192  dfsb2  2530  dfsb2ALT  2588  mooran1  2636  2eu3OLD  2738  eueq3  3705  sbcor  3825  sspss  4079  sspsstr  4085  elun  4128  ssun  4168  inss  4218  raaan2  4466  ifbi  4490  ifcomnan  4523  elpr2  4587  rabsnifsb  4656  tpprceq3  4735  tppreqb  4736  pwpw0  4744  sssn  4757  snsssn  4770  preq12b  4779  prnebg  4784  preq12nebg  4791  elpr2elpr  4797  pwsnALT  4829  prproe  4834  3elpr2eq  4835  unissint  4897  zfpair  5317  propeqop  5393  propssopi  5394  opthhausdorff  5403  opthhausdorff0  5404  iunopeqop  5407  relsnb  5673  sotri2  5986  sotri3  5987  somincom  5991  ordssun  6287  onun2i  6303  unizlim  6304  onxpdisj  6307  tpres  6962  sorpssuni  7451  ordeleqon  7494  ordunisuc  7538  orduninsuc  7549  tfinds  7565  limomss  7576  limom  7586  soxp  7817  ressuppssdif  7845  tfr2b  8026  omopthi  8277  domnsym  8635  brwdom  9023  cantnfvalf  9120  djuss  9341  djuunxp  9342  eldju2ndl  9345  eldju2ndr  9346  djuun  9347  updjud  9355  iscard3  9511  cflim2  9677  sornom  9691  isfin5  9713  isfin6  9714  sdom2en01  9716  fin23lem29  9755  fin23lem30  9756  fin56  9807  fin67  9809  hsmexlem9  9839  axcc4dom  9855  axdc3lem2  9865  axdc3lem4  9867  brdom3  9942  winainflem  10107  r1tskina  10196  indpi  10321  ltxrlt  10703  nn0sub  11939  nn0n0n1ge2b  11955  nn0ge2m1nn  11956  xnn0xr  11964  xnn0nemnf  11970  elnn0z  11986  nn0lt10b  12036  nn0le2is012  12038  nn0ind-raph  12074  uzin  12270  indstr2  12319  nn0ledivnn  12495  xrnemnf  12505  xrnepnf  12506  mnfltxr  12515  xnn0n0n1ge2b  12519  xnn0ge0  12521  xnn0xaddcl  12621  xnn0lenn0nn0  12631  xnn0xadd0  12633  xmullem2  12651  rexmul  12657  xnn0xrge0  12884  elfzonlteqm1  13106  elfznelfzo  13135  injresinjlem  13150  injresinj  13151  fldiv4p1lem1div2  13198  fldiv4lem1div2  13200  modfzo0difsn  13304  ssnn0fi  13346  fsuppmapnn0fiubex  13353  m1expcl2  13444  m1expeven  13469  sq01  13579  expnngt1  13595  nn0opthi  13623  facp1  13631  faclbnd3  13645  faclbnd4lem1  13646  faclbnd4lem3  13648  bcn1  13666  hashnemnf  13697  hashv01gt1  13698  hashneq0  13718  hashrabrsn  13726  hashrabsn01  13727  hashrabsn1  13728  hashunx  13740  hashsnle1  13771  hashfzp1  13785  hash2pwpr  13827  hashge2el2difr  13832  swrdnd2  14010  pfxnd0  14043  repswswrd  14139  relexpsucr  14381  relexpsucl  14385  relexpcnv  14387  relexprelg  14390  relexpdmg  14394  relexprng  14398  relexpfld  14401  relexpaddg  14405  sumz  15071  arisum  15207  arisum2  15208  pwdif  15215  ntrivcvg  15245  prod1  15290  fprodfac  15319  mod2eq1n2dvds  15688  mulsucdiv2z  15694  nn0o1gt2  15724  nno  15725  nn0o  15726  sumeven  15730  sumodd  15731  divalglem1  15737  divalglem6  15741  gcdaddmlem  15864  dfgcd2  15886  mulgcd  15888  lcmf  15969  lcmfunsnlem2lem2  15975  lcmfunsnlem2  15976  prm2orodd  16027  dfphi2  16103  nnnn0modprm0  16135  prm23lt5  16143  oddprmdvds  16231  4sqlem19  16291  ramz  16353  prmolefac  16374  prmgaplem7  16385  cshwshashlem1  16421  ressval3d  16553  firest  16698  xpsfeq  16828  funcres2c  17163  mulgnn0gsum  18166  symgfix2  18466  pmtrprfval  18537  m1expaddsub  18548  psgnprfval  18571  gsumpr  18997  gsumzunsnd  18998  sralem  19871  0ringnnzr  19963  frgpcyg  20636  cnmsgnsubg  20637  psgninv  20642  zrhpsgnelbas  20654  m2detleiblem1  21149  symgmatr01lem  21178  indiscld  21615  pnfnei  21744  mnfnei  21745  alexsubALTlem2  22572  alexsubALTlem3  22573  dscmet  23097  xrtgioo  23329  ishl2  23888  iunmbl2  24073  icombl  24080  ioombl  24081  recnprss  24417  recnperf  24418  dvexp2  24466  dvexp3  24490  dvne0f1  24524  plypf1  24717  taylfvallem1  24860  taylfval  24862  tayl0  24865  coseq0negpitopi  25004  logfac  25097  cxpexp  25164  pythag  25308  reasinsin  25387  harmonicbnd3  25499  lgslem4  25790  gausslemma2dlem0i  25854  lgsquadlem2  25871  2lgslem3  25894  2lgs  25897  2lgsoddprmlem3  25904  2sqnn0  25928  2sqnn  25929  cchhllem  26587  lfgrnloop  26824  uhgr2edg  26904  usgredg4  26913  usgredg2v  26923  usgrexmplef  26955  nb3grprlem1  27076  uvtx01vtx  27093  wlk1walk  27334  upgriswlk  27336  pthdadjvtx  27425  upgrwlkdvdelem  27431  pthdlem2lem  27462  2pthon3v  27636  clwwlkn  27718  clwwlkneq0  27721  eupth2lem3lem4  27924  konigsberg  27950  3vfriswmgrlem  27970  1to2vfriswmgr  27972  1to3vfriswmgr  27973  frgrregorufr0  28017  numclwlk1  28064  ex-pr  28123  shunssi  29059  cvmdi  30015  1neg1t1neg1  30386  iundisj2cnt  30435  fz1nnct  30439  xrge0iifiso  31064  esumpr2  31212  measiuns  31362  sxbrsigalem0  31415  bnj964  32101  subfacval3  32320  kur14lem7  32343  satfrnmapom  32501  gonar  32526  goalr  32528  mrsubcv  32641  nepss  32832  fz0n  32846  bccolsum  32855  dfon2lem7  32918  trpredlem1  32950  trpred0  32959  sltres  33053  nolesgn2o  33062  nosep1o  33070  altopthsn  33306  elhf2  33520  nn0prpw  33555  dissym1  33653  ordcmp  33679  bj-currypeirce  33776  bj-jaoi1  33788  bj-jaoi2  33789  bj-ififc  33799  bj-andnotim  33806  bj-nfimexal  33843  bj-sbsb  34044  bj-elsn12g  34234  bj-ideqg1  34335  finxpreclem2  34540  wl-equsal1i  34651  tan2h  34751  poimirlem23  34782  poimirlem32  34791  itg2addnclem  34810  orfa1  35231  orfa2  35232  imaexALTV  35455  inex3  35463  inxpex  35464  elpadd0  36812  sbor2  38969  sn-0ne2  39099  sn-0lt1  39108  hbtlem5  39589  rp-fakeimass  39739  rp-isfinite6  39745  pr2cv  39768  iunrelexp0  39908  relexpss1d  39911  relexpmulg  39916  iunrelexpmin2  39918  relexp01min  39919  relexp0a  39922  relexpxpmin  39923  relexpaddss  39924  clsk1indlem3  40254  ssrecnpr  40501  seff  40502  sblpnf  40503  expgrowthi  40526  dvconstbi  40527  19.33-2  40575  ax6e2ndeq  40754  en3lpVD  41040  undif3VD  41077  ax6e2ndeqVD  41104  ax6e2ndeqALT  41126  iooinlbub  41637  elprneb  43126  euoreqb  43170  2reu3  43171  afvpcfv0  43207  afvfv0bi  43213  afvco2  43237  afv2orxorb  43289  afv2ndeffv0  43321  afv2fv0b  43327  fvmptrabdm  43354  iccpartltu  43413  iccpartgtl  43414  iccpartgt  43415  iccpartleu  43416  iccpartgel  43417  iccpartnel  43426  elsprel  43465  prsprel  43477  sprsymrelfolem2  43483  paireqne  43501  odz2prm2pw  43553  fmtnofac1  43560  fmtno4prmfac  43562  31prm  43588  lighneallem2  43599  lighneallem3  43600  lighneallem4b  43602  lighneallem4  43603  zeo2ALTV  43664  nn0o1gt2ALTV  43687  nn0oALTV  43689  stgoldbwt  43769  sbgoldbwt  43770  sbgoldbalt  43774  sbgoldbm  43777  sbgoldbo  43780  nnsum3primesle9  43787  nnsum4primeseven  43793  nnsum4primesevenALTV  43794  wtgoldbnnsum4prm  43795  bgoldbnnsum3prm  43797  bgoldbtbndlem1  43798  bgoldbtbnd  43802  tgoldbach  43810  isomuspgrlem1  43820  upgrwlkupwlk  43843  ztprmneprm  44223  islinindfis  44332  lindslinindsimp2lem5  44345  lindslinindsimp2  44346  lindsrng01  44351  elfzolborelfzop1  44402  flnn0div2ge  44421  blennn0elnn  44465  blen1b  44476  nnolog2flm1  44478  blengt1fldiv2p1  44481  0dig2pr01  44498  dignn0flhalf  44506  nn0sumshdiglemB  44508  nn0sumshdiglem1  44509  resum2sqorgt0  44524  rrx2xpref1o  44533  rrx2plord2  44537  itsclc0yqsol  44579
  Copyright terms: Public domain W3C validator