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  1884  19.33b  1885  nfim1  2200  dfsb2  2491  mooran1  2548  eueq3  3671  sbcor  3793  sspss  4053  sspsstr  4059  elun  4104  ssun  4146  inss  4199  raaan2  4472  ifbi  4499  ifcomnan  4533  rabsnifsb  4674  tpprceq3  4755  tppreqb  4756  pwpw0  4764  sssn  4777  snsssn  4792  preq12b  4801  prnebg  4807  preq12nebg  4814  elpr2elpr  4820  prproe  4856  3elpr2eq  4857  unissint  4922  zfpair  5360  propeqop  5450  propssopi  5451  opthhausdorff  5460  opthhausdorff0  5461  iunopeqop  5464  relsnb  5745  iresn0n0  6005  sotri2  6078  sotri3  6079  somincom  6083  ordssun  6411  unizlim  6431  onxpdisj  6434  tpres  7137  sorpssuni  7668  ordeleqon  7718  ordunisuc  7765  orduninsuc  7776  tfinds  7793  limomss  7804  limom  7815  soxp  8062  ressuppssdif  8118  tfr2b  8318  omopthi  8579  domnsym  9020  brwdom  9459  cantnfvalf  9561  ttrclselem1  9621  djuss  9816  djuunxp  9817  eldju2ndl  9820  eldju2ndr  9821  djuun  9822  updjud  9830  iscard3  9987  cflim2  10157  sornom  10171  isfin5  10193  isfin6  10194  sdom2en01  10196  fin23lem29  10235  fin23lem30  10236  fin56  10287  fin67  10289  hsmexlem9  10319  axcc4dom  10335  axdc3lem2  10345  axdc3lem4  10347  brdom3  10422  winainflem  10587  r1tskina  10676  indpi  10801  ltxrlt  11186  nn0sub  12434  nn0n0n1ge2b  12453  nn0ge2m1nn  12454  xnn0xr  12462  xnn0nemnf  12468  elnn0z  12484  nn0lt10b  12538  nn0le2is012  12540  nn0ind-raph  12576  uzin  12775  indstr2  12828  nn0ledivnn  13008  xrnemnf  13019  xrnepnf  13020  mnfltxr  13029  xnn0n0n1ge2b  13034  xnn0ge0  13036  xnn0xaddcl  13137  xnn0lenn0nn0  13147  xnn0xadd0  13149  xmullem2  13167  rexmul  13173  xnn0xrge0  13409  elfzonlteqm1  13644  elfznelfzo  13675  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  14562  pfxnd0  14595  repswswrd  14690  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  smndex1basss  18779  smndex1mgm  18781  smndex1mndlem  18783  mulgnn0gsum  18959  symgfix2  19295  pmtrprfval  19366  m1expaddsub  19377  psgnprfval  19400  gsumpr  19834  gsumzunsnd  19835  0ringnnzr  20410  frgpcyg  21480  cnmsgnsubg  21484  psgninv  21489  zrhpsgnelbas  21501  m2detleiblem1  22509  symgmatr01lem  22538  indiscld  22976  pnfnei  23105  mnfnei  23106  alexsubALTlem2  23933  alexsubALTlem3  23934  dscmet  24458  xrtgioo  24693  ishl2  25268  iunmbl2  25456  icombl  25463  ioombl  25464  recnprss  25803  recnperf  25804  dvexp2  25856  dvexp3  25880  dvne0f1  25915  plypf1  26115  taylfvallem1  26262  taylfval  26264  tayl0  26267  coseq0negpitopi  26410  logfac  26508  cxpexp  26575  pythag  26725  reasinsin  26804  harmonicbnd3  26916  lgslem4  27209  gausslemma2dlem0i  27273  lgsquadlem2  27290  2lgslem3  27313  2lgs  27316  2lgsoddprmlem3  27323  2sqnn0  27347  2sqnn  27348  sltres  27572  nolesgn2o  27581  nogesgn1o  27583  nosep1o  27591  nosep2o  27592  noetalem2  27652  ssltun1  27719  ssltun2  27720  eln0s  28256  n0zs  28282  lfgrnloop  29070  uhgr2edg  29153  usgredg4  29162  usgredg2v  29172  usgrexmplef  29204  nb3grprlem1  29325  uvtx01vtx  29342  wlk1walk  29584  upgriswlk  29586  pthdadjvtx  29673  upgrwlkdvdelem  29681  pthdlem2lem  29712  pthspthcyc  29748  2pthon3v  29888  clwwlkn  29970  clwwlkneq0  29973  eupth2lem3lem4  30175  konigsberg  30201  3vfriswmgrlem  30221  1to2vfriswmgr  30223  1to3vfriswmgr  30224  frgrregorufr0  30268  numclwlk1  30315  ex-pr  30374  shunssi  31312  cvmdi  32268  1neg1t1neg1  32681  iundisj2cnt  32742  fz1nnct  32746  xrge0iifiso  33902  esumpr2  34034  measiuns  34184  sxbrsigalem0  34239  bnj964  34910  subfacval3  35162  kur14lem7  35185  satfrnmapom  35343  gonar  35368  goalr  35370  mrsubcv  35483  nepss  35691  nnuni  35700  fz0n  35704  bccolsum  35712  dfon2lem7  35763  altopthsn  35935  elhf2  36149  nn0prpw  36297  dissym1  36395  ordcmp  36421  bj-currypeirce  36531  bj-jaoi1  36545  bj-jaoi2  36546  bj-ififc  36556  bj-andnotim  36562  bj-nfimexal  36600  bj-sbsb  36811  bj-elsn12g  37034  bj-ideqg1  37138  finxpreclem2  37364  wl-equsal1i  37518  tan2h  37592  poimirlem23  37623  poimirlem32  37632  itg2addnclem  37651  orfa1  38065  orfa2  38066  inex3  38306  inxpex  38307  mopickr  38331  disjlem14  38776  elpadd0  39788  aks6d1c2p2  42092  sbor2  42185  sn-0ne2  42379  sn-0lt1  42448  hbtlem5  43101  omabs2  43305  safesnsupfiss  43388  safesnsupfidom1o  43390  safesnsupfilb  43391  rp-fakeimass  43485  rp-isfinite6  43491  pr2cv  43521  iunrelexp0  43675  relexpss1d  43678  relexpmulg  43683  iunrelexpmin2  43685  relexp01min  43686  relexp0a  43689  relexpxpmin  43690  relexpaddss  43691  clsk1indlem3  44016  ssrecnpr  44281  seff  44282  sblpnf  44283  expgrowthi  44306  dvconstbi  44307  19.33-2  44355  ax6e2ndeq  44533  en3lpVD  44818  undif3VD  44855  ax6e2ndeqVD  44882  ax6e2ndeqALT  44904  iooinlbub  45482  elprneb  47013  euoreqb  47093  2reu3  47094  afvpcfv0  47130  afvfv0bi  47136  afvco2  47160  afv2orxorb  47212  afv2ndeffv0  47244  afv2fv0b  47250  fvmptrabdm  47277  2ltceilhalf  47312  ceilhalfnn  47320  minusmodnep2tmod  47337  iccpartltu  47409  iccpartgtl  47410  iccpartgt  47411  iccpartleu  47412  iccpartgel  47413  iccpartnel  47422  elsprel  47459  prsprel  47471  sprsymrelfolem2  47477  paireqne  47495  odz2prm2pw  47547  fmtnofac1  47554  fmtno4prmfac  47556  31prm  47581  lighneallem2  47590  lighneallem3  47591  lighneallem4b  47593  lighneallem4  47594  zeo2ALTV  47655  nn0o1gt2ALTV  47678  nn0oALTV  47680  stgoldbwt  47760  sbgoldbwt  47761  sbgoldbalt  47765  sbgoldbm  47768  sbgoldbo  47771  nnsum3primesle9  47778  nnsum4primeseven  47784  nnsum4primesevenALTV  47785  wtgoldbnnsum4prm  47786  bgoldbnnsum3prm  47788  bgoldbtbndlem1  47789  bgoldbtbnd  47793  tgoldbach  47801  vopnbgrelself  47839  clnbgrgrim  47918  grtriproplem  47923  grtrif1o  47926  grtriclwlk3  47929  gpgedgvtx0  48045  gpgcubic  48063  gpg5nbgr3star  48065  gpgprismgr4cycllem3  48081  gpgprismgr4cycllem7  48085  gpgprismgr4cycllem10  48088  pgnbgreunbgrlem3  48102  pgnbgreunbgrlem6  48108  pgnbgreunbgr  48109  upgrwlkupwlk  48124  ztprmneprm  48331  islinindfis  48434  lindslinindsimp2lem5  48447  lindslinindsimp2  48448  lindsrng01  48453  elfzolborelfzop1  48504  flnn0div2ge  48518  blennn0elnn  48562  blen1b  48573  nnolog2flm1  48575  blengt1fldiv2p1  48578  0dig2pr01  48595  dignn0flhalf  48603  nn0sumshdiglemB  48605  nn0sumshdiglem1  48606  resum2sqorgt0  48694  rrx2xpref1o  48703  rrx2plord2  48707  itsclc0yqsol  48749  mosssn  48799  mo0sn  48800  mofsssn  48830  mofmo  48831  f1omo  48877  f1omoOLD  48878