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

Theorem jaoi 837
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 830 . . 3 ((𝜑𝜒) → (¬ 𝜑𝜒))
2 jaoi.2 . . 3 (𝜒𝜓)
31, 2syl6 35 . 2 ((𝜑𝜒) → (¬ 𝜑𝜓))
4 jaoi.1 . 2 (𝜑𝜓)
53, 4pm2.61d2 173 1 ((𝜑𝜒) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 826
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  df-or 827
This theorem is referenced by:  jao1i  838  jaod  839  pm1.4  849  pm1.2  869  pm2.4  872  pm2.41  873  orim12i  874  pm1.5  884  jaoa  926  pm2.42  929  pm4.44  930  jaoian  937  pm3.2ni  960  andi  967  annotanannotOLD  990  ecase3  1017  cases2ALT  1033  consensus  1039  jaoi3  1047  1fpid3  1065  19.33  1963  19.33b  1964  nfim1  2220  dfsb2  2519  mooran1  2675  2eu3  2703  eueq3  3531  sbcor  3629  sspss  3854  sspsstr  3860  elun  3902  ssun  3941  inss  3989  ifbi  4244  ifcomnan  4274  elpr2  4337  rabsnifsb  4391  tpprceq3  4468  tppreqb  4469  pwpw0  4477  sssn  4490  snsssn  4503  preq12b  4511  prnebg  4518  preq12nebg  4527  elpr2elpr  4533  pwsnALT  4565  prproe  4570  3elpr2eq  4571  unissint  4633  zfpair  5032  propeqop  5100  propssopi  5101  opthhausdorff  5110  opthhausdorff0  5111  iunopeqop  5114  sotri2  5666  sotri3  5667  somincom  5671  ordelinelOLD  5969  ordssun  5970  onun2i  5986  unizlim  5987  onxpdisj  5990  fvfundmfvn0  6367  tpres  6609  sorpssuni  7092  sorpssint  7093  ordeleqon  7134  ordunisuc  7178  orduninsuc  7189  tfinds  7205  limomss  7216  limom  7226  soxp  7440  ressuppssdif  7466  tfr2b  7644  omopthi  7890  domnsym  8241  brwdom  8627  cantnfvalf  8725  djuss  8945  djuunxp  8946  eldju2ndl  8949  eldju2ndr  8950  djuun  8951  updjud  8959  iscard3  9115  cflim2  9286  sornom  9300  isfin5  9322  isfin6  9323  sdom2en01  9325  fin23lem29  9364  fin23lem30  9365  fin56  9416  fin67  9418  hsmexlem9  9448  axcc4dom  9464  axdc3lem2  9474  axdc3lem4  9476  brdom3  9551  winainflem  9716  r1tskina  9805  indpi  9930  ltxrlt  10309  ltlen  10339  elnnnn0b  11538  nn0sub  11544  nn0n0n1ge2b  11560  nn0ge2m1nn  11561  xnn0xr  11569  xnn0nemnf  11575  elnn0z  11591  nn0lt10b  11640  nn0le2is012  11642  nn0ind-raph  11678  znnn0nn  11690  uzin  11921  indstr2  11969  nn0ledivnn  12145  xrnemnf  12155  xrnepnf  12156  mnfltxr  12165  xnn0n0n1ge2b  12169  xnn0ge0  12171  nn0pnfge0OLD  12172  xnn0xaddcl  12270  xnn0lenn0nn0  12279  xnn0xadd0  12281  xmullem2  12299  rexmul  12305  xnn0xrge0  12531  elfzonlteqm1  12751  elfznelfzo  12780  injresinjlem  12795  injresinj  12796  fldiv4p1lem1div2  12843  fldiv4lem1div2  12845  modfzo0difsn  12949  ssnn0fi  12991  fsuppmapnn0fiubex  12998  m1expcl2  13088  m1expeven  13113  sq01  13192  nn0opthi  13260  facp1  13268  faclbnd3  13282  faclbnd4lem1  13283  faclbnd4lem3  13285  bcn1  13303  hashnemnf  13335  hashv01gt1  13336  hashneq0  13356  hashrabrsn  13362  hashrabsn01  13363  hashrabsn1  13364  hashunx  13376  hashsnle1  13406  hashfzp1  13419  hash2pwpr  13459  hashge2el2difr  13464  swrdnd2  13641  repswswrd  13739  scshwfzeqfzo  13780  relexpsucr  13976  relexpsucl  13980  relexpcnv  13982  relexprelg  13985  relexpdmg  13989  relexprng  13993  relexpfld  13996  relexpaddg  14000  sumz  14660  arisum  14798  arisum2  14799  ntrivcvg  14835  prod1  14880  fprodfac  14909  mod2eq1n2dvds  15278  mulsucdiv2z  15284  nn0o1gt2  15304  nno  15305  nn0o  15306  sumeven  15317  sumodd  15318  divalglem1  15324  divalglem6  15328  gcdaddmlem  15452  dfgcd2  15470  mulgcd  15472  lcmf  15553  lcmfunsnlem2lem2  15559  lcmfunsnlem2  15560  prm2orodd  15610  dfphi2  15685  nnnn0modprm0  15717  prm23lt5  15725  oddprmdvds  15813  4sqlem19  15873  ramz  15935  prmolefac  15956  prmgaplem7  15967  cshwshashlem1  16008  ressval3d  16143  ressval3dOLD  16144  firest  16300  xpsfeq  16431  xpsfrnel2  16432  funcres2c  16767  symgfix2  18042  pmtrprfval  18113  m1expaddsub  18124  psgnprfval  18147  gsumzunsnd  18561  sralem  19391  0ringnnzr  19483  prmirred  20057  frgpcyg  20136  cnmsgnsubg  20137  psgninv  20142  zrhpsgnelbas  20155  m2detleiblem1  20647  symgmatr01lem  20677  pmatcollpw3fi1  20812  indiscld  21115  pnfnei  21244  mnfnei  21245  alexsubALTlem2  22071  alexsubALTlem3  22072  dscmet  22596  xrtgioo  22828  ishl2  23384  iunmbl2  23544  icombl  23551  ioombl  23552  recnprss  23887  recnperf  23888  dvexp2  23936  dvexp3  23960  dvne0f1  23994  plypf1  24187  taylfvallem1  24330  taylfval  24332  tayl0  24335  coseq0negpitopi  24475  logfac  24567  cxpexp  24634  pythag  24767  reasinsin  24843  harmonicbnd3  24954  lgslem4  25245  gausslemma2dlem0i  25309  lgsquadlem2  25326  2lgslem3  25349  2lgs  25352  2lgsoddprmlem3  25359  cchhllem  25987  lfgrnloop  26240  uhgr2edg  26321  usgredg4  26330  usgredg2v  26340  usgrexmplef  26373  nb3grprlem1  26504  uvtx01vtx  26524  uvtxa01vtx0OLD  26526  wlk1walk  26769  upgriswlk  26771  pthdadjvtx  26860  upgrwlkdvdelem  26866  pthdlem2lem  26897  2pthon3v  27087  clwwlknclwwlkdifsOLD  27126  clwwlkn  27175  clwwlkneq0  27180  eupth2lem3lem4  27408  konigsberg  27434  3vfriswmgrlem  27456  1to2vfriswmgr  27458  1to3vfriswmgr  27459  frgrregorufr0  27503  numclwlk1  27557  ex-pr  27623  shunssi  28561  cvmdi  29517  1neg1t1neg1  29848  iundisj2cnt  29892  fz1nnct  29894  xrge0iifiso  30315  esumpr2  30463  measiuns  30614  sxbrsigalem0  30667  bnj964  31345  subfacval3  31503  kur14lem7  31526  mrsubcv  31739  nepss  31931  fz0n  31948  bccolsum  31957  dfon2lem7  32024  trpredlem1  32057  trpred0  32066  sltres  32146  nolesgn2o  32155  nosep1o  32163  altopthsn  32399  elhf2  32613  nn0prpw  32649  dissym1  32751  ordcmp  32777  bj-jaoi1  32887  bj-jaoi2  32888  bj-andnotim  32904  bj-sbsb  33153  finxpreclem2  33557  wl-equsal1i  33657  tan2h  33727  poimirlem23  33758  poimirlem32  33767  itg2addnclem  33786  orfa1  34211  orfa2  34212  inex3  34442  inxpex  34443  elpadd0  35610  hbtlem5  38217  rp-fakeimass  38376  rp-isfinite6  38383  iunrelexp0  38513  relexpss1d  38516  relexpmulg  38521  iunrelexpmin2  38523  relexp01min  38524  relexp0a  38527  relexpxpmin  38528  relexpaddss  38529  clsk1indlem3  38860  ssrecnpr  39026  seff  39027  sblpnf  39028  expgrowthi  39051  dvconstbi  39052  19.33-2  39100  ax6e2ndeq  39294  en3lpVD  39596  undif3VD  39634  ax6e2ndeqVD  39661  ax6e2ndeqALT  39683  iooinlbub  40238  raaan2  41689  2reu3  41702  afvpcfv0  41740  afvfv0bi  41746  afvco2  41770  elprneb  41813  fvmptrabdm  41825  iccpartltu  41879  iccpartgtl  41880  iccpartgt  41881  iccpartleu  41882  iccpartgel  41883  iccpartnel  41892  odz2prm2pw  41993  fmtnofac1  42000  fmtno4prmfac  42002  pwdif  42019  31prm  42030  lighneallem2  42041  lighneallem3  42042  lighneallem4b  42044  lighneallem4  42045  zeo2ALTV  42100  nn0o1gt2ALTV  42123  nn0oALTV  42125  stgoldbwt  42182  sbgoldbwt  42183  sbgoldbalt  42187  sbgoldbm  42190  sbgoldbo  42193  nnsum3primesle9  42200  nnsum4primeseven  42206  nnsum4primesevenALTV  42207  wtgoldbnnsum4prm  42208  bgoldbnnsum3prm  42210  bgoldbtbndlem1  42211  bgoldbtbnd  42215  tgoldbach  42223  tgoldbachOLD  42230  upgrwlkupwlk  42239  elsprel  42243  prsprel  42255  sprsymrelfolem2  42261  ztprmneprm  42643  gsumpr  42657  islinindfis  42756  lindslinindsimp2lem5  42769  lindslinindsimp2  42770  lindsrng01  42775  elfzolborelfzop1  42827  flnn0div2ge  42845  blennn0elnn  42889  blen1b  42900  nnolog2flm1  42902  blengt1fldiv2p1  42905  0dig2pr01  42922  dignn0flhalf  42930  nn0sumshdiglemB  42932  nn0sumshdiglem1  42933
  Copyright terms: Public domain W3C validator