Theorem jaoi 858

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 852	. . 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 848

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 849

This theorem is referenced by:  jao1i  859  jaod  860  pm1.4  870  pm3.2ni  881  pm1.2  904  pm2.4  907  pm2.41  908  orim12i  909  pm1.5  920  pm2.42  945  jaoa  958  jaoian  959  pm4.44  999  andi  1010  ecase3  1033  cases2ALT  1049  consensus  1053  jaoi3  1061  1fpid3  1082  19.33  1886  19.33b  1887  nfim1  2207  dfsb2  2498  mooran1  2556  eueq3  3658  sbcor  3780  sspss  4043  sspsstr  4049  elun  4094  ssun  4136  inss  4189  raaan2  4463  ifbi  4490  ifcomnan  4524  rabsnifsb  4667  tpprceq3  4748  tppreqb  4749  pwpw0  4757  sssn  4770  snsssn  4785  preq12b  4794  prnebg  4800  preq12nebg  4807  elpr2elpr  4813  prproe  4849  3elpr2eq  4850  unissint  4915  zfpair  5356  axprg  5372  propeqop  5453  propssopi  5454  opthhausdorff  5463  opthhausdorff0  5464  iunopeqop  5467  relsnb  5749  iresn0n0  6011  sotri2  6084  sotri3  6085  somincom  6089  ordssun  6419  unizlim  6439  onxpdisj  6442  tpres  7147  sorpssuni  7677  ordeleqon  7727  ordunisuc  7774  orduninsuc  7785  tfinds  7802  limomss  7813  limom  7824  soxp  8070  ressuppssdif  8126  tfr2b  8326  omopthi  8588  domnsym  9032  ordfin  9141  brwdom  9473  cantnfvalf  9575  ttrclselem1  9635  djuss  9833  djuunxp  9834  eldju2ndl  9837  eldju2ndr  9838  djuun  9839  updjud  9847  iscard3  10004  cflim2  10174  sornom  10188  isfin5  10210  isfin6  10211  sdom2en01  10213  fin23lem29  10252  fin23lem30  10253  fin56  10304  fin67  10306  hsmexlem9  10336  axcc4dom  10352  axdc3lem2  10362  axdc3lem4  10364  brdom3  10439  winainflem  10605  r1tskina  10694  indpi  10819  ltxrlt  11205  nn0sub  12476  nn0n0n1ge2b  12495  nn0ge2m1nn  12496  xnn0xr  12504  xnn0nemnf  12510  elnn0z  12526  nn0lt10b  12580  nn0le2is012  12582  nn0ind-raph  12618  uzin  12813  indstr2  12866  nn0ledivnn  13046  xrnemnf  13057  xrnepnf  13058  mnfltxr  13067  xnn0n0n1ge2b  13072  xnn0ge0  13074  xnn0xaddcl  13176  xnn0lenn0nn0  13186  xnn0xadd0  13188  xmullem2  13206  rexmul  13212  xnn0xrge0  13448  elfzonlteqm1  13685  elfznelfzo  13717  injresinjlem  13734  injresinj  13735  fldiv4p1lem1div2  13783  fldiv4lem1div2  13785  modfzo0difsn  13894  ssnn0fi  13936  fsuppmapnn0fiubex  13943  m1expcl2  14036  m1expeven  14060  zzlesq  14157  sq01  14176  expnngt1  14192  nn0opthi  14221  facp1  14229  faclbnd3  14243  faclbnd4lem1  14244  faclbnd4lem3  14246  bcn1  14264  hashnemnf  14295  hashv01gt1  14296  hashneq0  14315  hashrabrsn  14323  hashrabsn01  14324  hashrabsn1  14325  hashunx  14337  hashsnle1  14368  hashfzp1  14382  hash2pwpr  14427  hashge2el2difr  14432  swrdnd2  14607  pfxnd0  14640  repswswrd  14735  relexpsucl  14982  relexpsucr  14983  relexpcnv  14986  relexprelg  14989  relexpdmg  14993  relexprng  14997  relexpfld  15000  relexpaddg  15004  sumz  15673  arisum  15814  arisum2  15815  pwdif  15822  ntrivcvg  15851  prod1  15898  fprodfac  15927  mod2eq1n2dvds  16305  mulsucdiv2z  16311  nn0o1gt2  16339  nno  16340  nn0o  16341  sumeven  16345  sumodd  16346  divalglem1  16352  divalglem6  16356  gcdaddmlem  16482  dfgcd2  16504  mulgcd  16506  lcmf  16591  lcmfunsnlem2lem2  16597  lcmfunsnlem2  16598  prm2orodd  16649  dfphi2  16733  nnnn0modprm0  16766  prm23lt5  16774  oddprmdvds  16863  4sqlem19  16923  ramz  16985  prmolefac  17006  prmgaplem7  17017  cshwshashlem1  17055  ressval3d  17205  firest  17384  xpsfeq  17516  funcres2c  17859  ex-chn2  18593  smndex1basss  18865  smndex1mgm  18867  smndex1mndlem  18869  mulgnn0gsum  19045  symgfix2  19380  pmtrprfval  19451  m1expaddsub  19462  psgnprfval  19485  gsumpr  19919  gsumzunsnd  19920  0ringnnzr  20491  frgpcyg  21561  cnmsgnsubg  21565  psgninv  21570  zrhpsgnelbas  21582  m2detleiblem1  22598  symgmatr01lem  22627  indiscld  23065  pnfnei  23194  mnfnei  23195  alexsubALTlem2  24022  alexsubALTlem3  24023  dscmet  24546  xrtgioo  24781  ishl2  25346  iunmbl2  25533  icombl  25540  ioombl  25541  recnprss  25880  recnperf  25881  dvexp2  25930  dvexp3  25954  dvne0f1  25989  plypf1  26189  taylfvallem1  26335  taylfval  26337  tayl0  26340  coseq0negpitopi  26483  logfac  26581  cxpexp  26648  pythag  26798  reasinsin  26877  harmonicbnd3  26989  lgslem4  27282  gausslemma2dlem0i  27346  lgsquadlem2  27363  2lgslem3  27386  2lgs  27389  2lgsoddprmlem3  27396  2sqnn0  27420  2sqnn  27421  ltsres  27645  nolesgn2o  27654  nogesgn1o  27656  nosep1o  27664  nosep2o  27665  noetalem2  27725  sltsun1  27799  sltsun2  27800  eln0s  28372  n0zs  28400  bdaypw2n0bndlem  28474  bdaypw2n0bnd  28475  lfgrnloop  29213  uhgr2edg  29296  usgredg4  29305  usgredg2v  29315  usgrexmplef  29347  nb3grprlem1  29468  uvtx01vtx  29485  wlk1walk  29727  upgriswlk  29729  pthdadjvtx  29816  upgrwlkdvdelem  29824  pthdlem2lem  29855  pthspthcyc  29891  2pthon3v  30031  clwwlkn  30116  clwwlkneq0  30119  eupth2lem3lem4  30321  konigsberg  30347  3vfriswmgrlem  30367  1to2vfriswmgr  30369  1to3vfriswmgr  30370  frgrregorufr0  30414  numclwlk1  30461  ex-pr  30520  shunssi  31459  cvmdi  32415  1neg1t1neg1  32831  iundisj2cnt  32892  fz1nnct  32894  xrge0iifiso  34100  esumpr2  34232  measiuns  34382  sxbrsigalem0  34436  bnj964  35106  subfacval3  35392  kur14lem7  35415  satfrnmapom  35573  gonar  35598  goalr  35600  mrsubcv  35713  nepss  35921  nnuni  35930  fz0n  35934  bccolsum  35942  dfon2lem7  35990  altopthsn  36164  elhf2  36378  nn0prpw  36526  dissym1  36624  ordcmp  36650  ttciunun  36714  bj-currypeirce  36834  bj-jaoi1  36849  bj-jaoi2  36850  bj-ififc  36860  bj-andnotim  36866  bj-nfimexal  36916  bj-sbsb  37157  bj-elsn12g  37380  bj-ideqg1  37491  finxpreclem2  37717  wl-equsal1i  37880  tan2h  37944  poimirlem23  37975  poimirlem32  37984  itg2addnclem  38003  orfa1  38417  orfa2  38418  inex3  38670  inxpex  38671  mopickr  38703  disjlem14  39233  elpadd0  40266  aks6d1c2p2  42569  sbor2  42662  sn-0ne2  42849  sn-0lt1  42931  hbtlem5  43571  omabs2  43775  safesnsupfiss  43857  safesnsupfidom1o  43859  safesnsupfilb  43860  rp-fakeimass  43954  rp-isfinite6  43960  pr2cv  43990  iunrelexp0  44144  relexpss1d  44147  relexpmulg  44152  iunrelexpmin2  44154  relexp01min  44155  relexp0a  44158  relexpxpmin  44159  relexpaddss  44160  clsk1indlem3  44485  ssrecnpr  44750  seff  44751  sblpnf  44752  expgrowthi  44775  dvconstbi  44776  19.33-2  44824  ax6e2ndeq  45001  en3lpVD  45286  undif3VD  45323  ax6e2ndeqVD  45350  ax6e2ndeqALT  45372  iooinlbub  45946  elprneb  47474  euoreqb  47554  2reu3  47555  afvpcfv0  47591  afvfv0bi  47597  afvco2  47621  afv2orxorb  47673  afv2ndeffv0  47705  afv2fv0b  47711  fvmptrabdm  47738  nnmul2  47775  2ltceilhalf  47777  ceilhalfnn  47785  minusmodnep2tmod  47804  iccpartltu  47882  iccpartgtl  47883  iccpartgt  47884  iccpartleu  47885  iccpartgel  47886  iccpartnel  47895  elsprel  47932  prsprel  47944  sprsymrelfolem2  47950  paireqne  47968  odz2prm2pw  48023  fmtnofac1  48030  fmtno4prmfac  48032  31prm  48057  lighneallem2  48066  lighneallem3  48067  lighneallem4b  48069  lighneallem4  48070  ppivalnnnprm  48088  ppivalnn  48092  zeo2ALTV  48144  nn0o1gt2ALTV  48167  nn0oALTV  48169  stgoldbwt  48249  sbgoldbwt  48250  sbgoldbalt  48254  sbgoldbm  48257  sbgoldbo  48260  nnsum3primesle9  48267  nnsum4primeseven  48273  nnsum4primesevenALTV  48274  wtgoldbnnsum4prm  48275  bgoldbnnsum3prm  48277  bgoldbtbndlem1  48278  bgoldbtbnd  48282  tgoldbach  48290  vopnbgrelself  48328  clnbgrgrim  48407  grtriproplem  48412  grtrif1o  48415  grtriclwlk3  48418  gpgedgvtx0  48534  gpgcubic  48552  gpg5nbgr3star  48554  gpgprismgr4cycllem3  48570  gpgprismgr4cycllem7  48574  gpgprismgr4cycllem10  48577  pgnbgreunbgrlem3  48591  pgnbgreunbgrlem6  48597  pgnbgreunbgr  48598  upgrwlkupwlk  48613  ztprmneprm  48820  islinindfis  48922  lindslinindsimp2lem5  48935  lindslinindsimp2  48936  lindsrng01  48941  elfzolborelfzop1  48992  flnn0div2ge  49006  blennn0elnn  49050  blen1b  49061  nnolog2flm1  49063  blengt1fldiv2p1  49066  0dig2pr01  49083  dignn0flhalf  49091  nn0sumshdiglemB  49093  nn0sumshdiglem1  49094  resum2sqorgt0  49182  rrx2xpref1o  49191  rrx2plord2  49195  itsclc0yqsol  49237  mosssn  49287  mo0sn  49288  mofsssn  49318  mofmo  49319  f1omo  49365  f1omoOLD  49366