Theorem jaoi 857

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

Step	Hyp	Ref	Expression
1		pm2.53 851	. . 3 ⊢ ((𝜑 ∨ 𝜒) → (¬ 𝜑 → 𝜒))
2		jaoi.2	. . 3 ⊢ (𝜒 → 𝜓)
3	1, 2	syl6 35	. 2 ⊢ ((𝜑 ∨ 𝜒) → (¬ 𝜑 → 𝜓))
4		jaoi.1	. 2 ⊢ (𝜑 → 𝜓)
5	3, 4	pm2.61d2 181	1 ⊢ ((𝜑 ∨ 𝜒) → 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 847

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 207  df-or 848

This theorem is referenced by:  jao1i  858  jaod  859  pm1.4  869  pm3.2ni  880  pm1.2  903  pm2.4  906  pm2.41  907  orim12i  908  pm1.5  919  pm2.42  944  jaoa  957  jaoian  958  pm4.44  998  andi  1009  ecase3  1032  cases2ALT  1048  consensus  1052  jaoi3  1060  1fpid3  1081  19.33  1885  19.33b  1886  nfim1  2202  dfsb2  2493  mooran1  2550  eueq3  3665  sbcor  3787  sspss  4049  sspsstr  4055  elun  4100  ssun  4142  inss  4195  raaan2  4468  ifbi  4495  ifcomnan  4529  rabsnifsb  4672  tpprceq3  4753  tppreqb  4754  pwpw0  4762  sssn  4775  snsssn  4790  preq12b  4799  prnebg  4805  preq12nebg  4812  elpr2elpr  4818  prproe  4854  3elpr2eq  4855  unissint  4920  zfpair  5357  propeqop  5445  propssopi  5446  opthhausdorff  5455  opthhausdorff0  5456  iunopeqop  5459  relsnb  5741  iresn0n0  6002  sotri2  6075  sotri3  6076  somincom  6080  ordssun  6410  unizlim  6430  onxpdisj  6433  tpres  7135  sorpssuni  7665  ordeleqon  7715  ordunisuc  7762  orduninsuc  7773  tfinds  7790  limomss  7801  limom  7812  soxp  8059  ressuppssdif  8115  tfr2b  8315  omopthi  8576  domnsym  9016  brwdom  9453  cantnfvalf  9555  ttrclselem1  9615  djuss  9813  djuunxp  9814  eldju2ndl  9817  eldju2ndr  9818  djuun  9819  updjud  9827  iscard3  9984  cflim2  10154  sornom  10168  isfin5  10190  isfin6  10191  sdom2en01  10193  fin23lem29  10232  fin23lem30  10233  fin56  10284  fin67  10286  hsmexlem9  10316  axcc4dom  10332  axdc3lem2  10342  axdc3lem4  10344  brdom3  10419  winainflem  10584  r1tskina  10673  indpi  10798  ltxrlt  11183  nn0sub  12431  nn0n0n1ge2b  12450  nn0ge2m1nn  12451  xnn0xr  12459  xnn0nemnf  12465  elnn0z  12481  nn0lt10b  12535  nn0le2is012  12537  nn0ind-raph  12573  uzin  12772  indstr2  12825  nn0ledivnn  13005  xrnemnf  13016  xrnepnf  13017  mnfltxr  13026  xnn0n0n1ge2b  13031  xnn0ge0  13033  xnn0xaddcl  13134  xnn0lenn0nn0  13144  xnn0xadd0  13146  xmullem2  13164  rexmul  13170  xnn0xrge0  13406  elfzonlteqm1  13641  elfznelfzo  13673  injresinjlem  13690  injresinj  13691  fldiv4p1lem1div2  13739  fldiv4lem1div2  13741  modfzo0difsn  13850  ssnn0fi  13892  fsuppmapnn0fiubex  13899  m1expcl2  13992  m1expeven  14016  zzlesq  14113  sq01  14132  expnngt1  14148  nn0opthi  14177  facp1  14185  faclbnd3  14199  faclbnd4lem1  14200  faclbnd4lem3  14202  bcn1  14220  hashnemnf  14251  hashv01gt1  14252  hashneq0  14271  hashrabrsn  14279  hashrabsn01  14280  hashrabsn1  14281  hashunx  14293  hashsnle1  14324  hashfzp1  14338  hash2pwpr  14383  hashge2el2difr  14388  swrdnd2  14563  pfxnd0  14596  repswswrd  14691  relexpsucl  14938  relexpsucr  14939  relexpcnv  14942  relexprelg  14945  relexpdmg  14949  relexprng  14953  relexpfld  14956  relexpaddg  14960  sumz  15629  arisum  15767  arisum2  15768  pwdif  15775  ntrivcvg  15804  prod1  15851  fprodfac  15880  mod2eq1n2dvds  16258  mulsucdiv2z  16264  nn0o1gt2  16292  nno  16293  nn0o  16294  sumeven  16298  sumodd  16299  divalglem1  16305  divalglem6  16309  gcdaddmlem  16435  dfgcd2  16457  mulgcd  16459  lcmf  16544  lcmfunsnlem2lem2  16550  lcmfunsnlem2  16551  prm2orodd  16602  dfphi2  16685  nnnn0modprm0  16718  prm23lt5  16726  oddprmdvds  16815  4sqlem19  16875  ramz  16937  prmolefac  16958  prmgaplem7  16969  cshwshashlem1  17007  ressval3d  17157  firest  17336  xpsfeq  17467  funcres2c  17810  ex-chn2  18544  smndex1basss  18813  smndex1mgm  18815  smndex1mndlem  18817  mulgnn0gsum  18993  symgfix2  19328  pmtrprfval  19399  m1expaddsub  19410  psgnprfval  19433  gsumpr  19867  gsumzunsnd  19868  0ringnnzr  20440  frgpcyg  21510  cnmsgnsubg  21514  psgninv  21519  zrhpsgnelbas  21531  m2detleiblem1  22539  symgmatr01lem  22568  indiscld  23006  pnfnei  23135  mnfnei  23136  alexsubALTlem2  23963  alexsubALTlem3  23964  dscmet  24487  xrtgioo  24722  ishl2  25297  iunmbl2  25485  icombl  25492  ioombl  25493  recnprss  25832  recnperf  25833  dvexp2  25885  dvexp3  25909  dvne0f1  25944  plypf1  26144  taylfvallem1  26291  taylfval  26293  tayl0  26296  coseq0negpitopi  26439  logfac  26537  cxpexp  26604  pythag  26754  reasinsin  26833  harmonicbnd3  26945  lgslem4  27238  gausslemma2dlem0i  27302  lgsquadlem2  27319  2lgslem3  27342  2lgs  27345  2lgsoddprmlem3  27352  2sqnn0  27376  2sqnn  27377  sltres  27601  nolesgn2o  27610  nogesgn1o  27612  nosep1o  27620  nosep2o  27621  noetalem2  27681  ssltun1  27749  ssltun2  27750  eln0s  28287  n0zs  28313  lfgrnloop  29103  uhgr2edg  29186  usgredg4  29195  usgredg2v  29205  usgrexmplef  29237  nb3grprlem1  29358  uvtx01vtx  29375  wlk1walk  29617  upgriswlk  29619  pthdadjvtx  29706  upgrwlkdvdelem  29714  pthdlem2lem  29745  pthspthcyc  29781  2pthon3v  29921  clwwlkn  30006  clwwlkneq0  30009  eupth2lem3lem4  30211  konigsberg  30237  3vfriswmgrlem  30257  1to2vfriswmgr  30259  1to3vfriswmgr  30260  frgrregorufr0  30304  numclwlk1  30351  ex-pr  30410  shunssi  31348  cvmdi  32304  1neg1t1neg1  32721  iundisj2cnt  32781  fz1nnct  32783  xrge0iifiso  33948  esumpr2  34080  measiuns  34230  sxbrsigalem0  34284  bnj964  34955  subfacval3  35233  kur14lem7  35256  satfrnmapom  35414  gonar  35439  goalr  35441  mrsubcv  35554  nepss  35762  nnuni  35771  fz0n  35775  bccolsum  35783  dfon2lem7  35831  altopthsn  36003  elhf2  36217  nn0prpw  36365  dissym1  36463  ordcmp  36489  bj-currypeirce  36599  bj-jaoi1  36613  bj-jaoi2  36614  bj-ififc  36624  bj-andnotim  36630  bj-nfimexal  36668  bj-sbsb  36879  bj-elsn12g  37102  bj-ideqg1  37206  finxpreclem2  37432  wl-equsal1i  37586  tan2h  37660  poimirlem23  37691  poimirlem32  37700  itg2addnclem  37719  orfa1  38133  orfa2  38134  inex3  38374  inxpex  38375  mopickr  38399  disjlem14  38844  elpadd0  39856  aks6d1c2p2  42160  sbor2  42253  sn-0ne2  42447  sn-0lt1  42516  hbtlem5  43169  omabs2  43373  safesnsupfiss  43456  safesnsupfidom1o  43458  safesnsupfilb  43459  rp-fakeimass  43553  rp-isfinite6  43559  pr2cv  43589  iunrelexp0  43743  relexpss1d  43746  relexpmulg  43751  iunrelexpmin2  43753  relexp01min  43754  relexp0a  43757  relexpxpmin  43758  relexpaddss  43759  clsk1indlem3  44084  ssrecnpr  44349  seff  44350  sblpnf  44351  expgrowthi  44374  dvconstbi  44375  19.33-2  44423  ax6e2ndeq  44600  en3lpVD  44885  undif3VD  44922  ax6e2ndeqVD  44949  ax6e2ndeqALT  44971  iooinlbub  45549  elprneb  47068  euoreqb  47148  2reu3  47149  afvpcfv0  47185  afvfv0bi  47191  afvco2  47215  afv2orxorb  47267  afv2ndeffv0  47299  afv2fv0b  47305  fvmptrabdm  47332  2ltceilhalf  47367  ceilhalfnn  47375  minusmodnep2tmod  47392  iccpartltu  47464  iccpartgtl  47465  iccpartgt  47466  iccpartleu  47467  iccpartgel  47468  iccpartnel  47477  elsprel  47514  prsprel  47526  sprsymrelfolem2  47532  paireqne  47550  odz2prm2pw  47602  fmtnofac1  47609  fmtno4prmfac  47611  31prm  47636  lighneallem2  47645  lighneallem3  47646  lighneallem4b  47648  lighneallem4  47649  zeo2ALTV  47710  nn0o1gt2ALTV  47733  nn0oALTV  47735  stgoldbwt  47815  sbgoldbwt  47816  sbgoldbalt  47820  sbgoldbm  47823  sbgoldbo  47826  nnsum3primesle9  47833  nnsum4primeseven  47839  nnsum4primesevenALTV  47840  wtgoldbnnsum4prm  47841  bgoldbnnsum3prm  47843  bgoldbtbndlem1  47844  bgoldbtbnd  47848  tgoldbach  47856  vopnbgrelself  47894  clnbgrgrim  47973  grtriproplem  47978  grtrif1o  47981  grtriclwlk3  47984  gpgedgvtx0  48100  gpgcubic  48118  gpg5nbgr3star  48120  gpgprismgr4cycllem3  48136  gpgprismgr4cycllem7  48140  gpgprismgr4cycllem10  48143  pgnbgreunbgrlem3  48157  pgnbgreunbgrlem6  48163  pgnbgreunbgr  48164  upgrwlkupwlk  48179  ztprmneprm  48386  islinindfis  48489  lindslinindsimp2lem5  48502  lindslinindsimp2  48503  lindsrng01  48508  elfzolborelfzop1  48559  flnn0div2ge  48573  blennn0elnn  48617  blen1b  48628  nnolog2flm1  48630  blengt1fldiv2p1  48633  0dig2pr01  48650  dignn0flhalf  48658  nn0sumshdiglemB  48660  nn0sumshdiglem1  48661  resum2sqorgt0  48749  rrx2xpref1o  48758  rrx2plord2  48762  itsclc0yqsol  48804  mosssn  48854  mo0sn  48855  mofsssn  48885  mofmo  48886  f1omo  48932  f1omoOLD  48933