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  2492  mooran1  2549  eueq3  3685  sbcor  3807  sspss  4068  sspsstr  4074  elun  4119  ssun  4161  inss  4214  raaan2  4487  ifbi  4514  ifcomnan  4548  rabsnifsb  4689  tpprceq3  4771  tppreqb  4772  pwpw0  4780  sssn  4793  snsssn  4808  preq12b  4817  prnebg  4823  preq12nebg  4830  elpr2elpr  4836  prproe  4872  3elpr2eq  4873  unissint  4939  zfpair  5379  propeqop  5470  propssopi  5471  opthhausdorff  5480  opthhausdorff0  5481  iunopeqop  5484  relsnb  5768  iresn0n0  6028  sotri2  6105  sotri3  6106  somincom  6110  ordssun  6439  unizlim  6460  onxpdisj  6463  tpres  7178  sorpssuni  7711  ordeleqon  7761  ordunisuc  7810  orduninsuc  7822  tfinds  7839  limomss  7850  limom  7861  soxp  8111  ressuppssdif  8167  tfr2b  8367  omopthi  8628  domnsym  9073  brwdom  9527  cantnfvalf  9625  ttrclselem1  9685  djuss  9880  djuunxp  9881  eldju2ndl  9884  eldju2ndr  9885  djuun  9886  updjud  9894  iscard3  10053  cflim2  10223  sornom  10237  isfin5  10259  isfin6  10260  sdom2en01  10262  fin23lem29  10301  fin23lem30  10302  fin56  10353  fin67  10355  hsmexlem9  10385  axcc4dom  10401  axdc3lem2  10411  axdc3lem4  10413  brdom3  10488  winainflem  10653  r1tskina  10742  indpi  10867  ltxrlt  11251  nn0sub  12499  nn0n0n1ge2b  12518  nn0ge2m1nn  12519  xnn0xr  12527  xnn0nemnf  12533  elnn0z  12549  nn0lt10b  12603  nn0le2is012  12605  nn0ind-raph  12641  uzin  12840  indstr2  12893  nn0ledivnn  13073  xrnemnf  13084  xrnepnf  13085  mnfltxr  13094  xnn0n0n1ge2b  13099  xnn0ge0  13101  xnn0xaddcl  13202  xnn0lenn0nn0  13212  xnn0xadd0  13214  xmullem2  13232  rexmul  13238  xnn0xrge0  13474  elfzonlteqm1  13709  elfznelfzo  13740  injresinjlem  13755  injresinj  13756  fldiv4p1lem1div2  13804  fldiv4lem1div2  13806  modfzo0difsn  13915  ssnn0fi  13957  fsuppmapnn0fiubex  13964  m1expcl2  14057  m1expeven  14081  zzlesq  14178  sq01  14197  expnngt1  14213  nn0opthi  14242  facp1  14250  faclbnd3  14264  faclbnd4lem1  14265  faclbnd4lem3  14267  bcn1  14285  hashnemnf  14316  hashv01gt1  14317  hashneq0  14336  hashrabrsn  14344  hashrabsn01  14345  hashrabsn1  14346  hashunx  14358  hashsnle1  14389  hashfzp1  14403  hash2pwpr  14448  hashge2el2difr  14453  swrdnd2  14627  pfxnd0  14660  repswswrd  14756  relexpsucl  15004  relexpsucr  15005  relexpcnv  15008  relexprelg  15011  relexpdmg  15015  relexprng  15019  relexpfld  15022  relexpaddg  15026  sumz  15695  arisum  15833  arisum2  15834  pwdif  15841  ntrivcvg  15870  prod1  15917  fprodfac  15946  mod2eq1n2dvds  16324  mulsucdiv2z  16330  nn0o1gt2  16358  nno  16359  nn0o  16360  sumeven  16364  sumodd  16365  divalglem1  16371  divalglem6  16375  gcdaddmlem  16501  dfgcd2  16523  mulgcd  16525  lcmf  16610  lcmfunsnlem2lem2  16616  lcmfunsnlem2  16617  prm2orodd  16668  dfphi2  16751  nnnn0modprm0  16784  prm23lt5  16792  oddprmdvds  16881  4sqlem19  16941  ramz  17003  prmolefac  17024  prmgaplem7  17035  cshwshashlem1  17073  ressval3d  17223  firest  17402  xpsfeq  17533  funcres2c  17872  smndex1basss  18839  smndex1mgm  18841  smndex1mndlem  18843  mulgnn0gsum  19019  symgfix2  19353  pmtrprfval  19424  m1expaddsub  19435  psgnprfval  19458  gsumpr  19892  gsumzunsnd  19893  0ringnnzr  20441  frgpcyg  21490  cnmsgnsubg  21493  psgninv  21498  zrhpsgnelbas  21510  m2detleiblem1  22518  symgmatr01lem  22547  indiscld  22985  pnfnei  23114  mnfnei  23115  alexsubALTlem2  23942  alexsubALTlem3  23943  dscmet  24467  xrtgioo  24702  ishl2  25277  iunmbl2  25465  icombl  25472  ioombl  25473  recnprss  25812  recnperf  25813  dvexp2  25865  dvexp3  25889  dvne0f1  25924  plypf1  26124  taylfvallem1  26271  taylfval  26273  tayl0  26276  coseq0negpitopi  26419  logfac  26517  cxpexp  26584  pythag  26734  reasinsin  26813  harmonicbnd3  26925  lgslem4  27218  gausslemma2dlem0i  27282  lgsquadlem2  27299  2lgslem3  27322  2lgs  27325  2lgsoddprmlem3  27332  2sqnn0  27356  2sqnn  27357  sltres  27581  nolesgn2o  27590  nogesgn1o  27592  nosep1o  27600  nosep2o  27601  noetalem2  27661  ssltun1  27727  ssltun2  27728  eln0s  28258  n0zs  28284  lfgrnloop  29059  uhgr2edg  29142  usgredg4  29151  usgredg2v  29161  usgrexmplef  29193  nb3grprlem1  29314  uvtx01vtx  29331  wlk1walk  29574  upgriswlk  29576  pthdadjvtx  29665  upgrwlkdvdelem  29673  pthdlem2lem  29704  pthspthcyc  29740  2pthon3v  29880  clwwlkn  29962  clwwlkneq0  29965  eupth2lem3lem4  30167  konigsberg  30193  3vfriswmgrlem  30213  1to2vfriswmgr  30215  1to3vfriswmgr  30216  frgrregorufr0  30260  numclwlk1  30307  ex-pr  30366  shunssi  31304  cvmdi  32260  1neg1t1neg1  32668  iundisj2cnt  32729  fz1nnct  32733  xrge0iifiso  33932  esumpr2  34064  measiuns  34214  sxbrsigalem0  34269  bnj964  34940  subfacval3  35183  kur14lem7  35206  satfrnmapom  35364  gonar  35389  goalr  35391  mrsubcv  35504  nepss  35712  nnuni  35721  fz0n  35725  bccolsum  35733  dfon2lem7  35784  altopthsn  35956  elhf2  36170  nn0prpw  36318  dissym1  36416  ordcmp  36442  bj-currypeirce  36552  bj-jaoi1  36566  bj-jaoi2  36567  bj-ififc  36577  bj-andnotim  36583  bj-nfimexal  36621  bj-sbsb  36832  bj-elsn12g  37055  bj-ideqg1  37159  finxpreclem2  37385  wl-equsal1i  37539  tan2h  37613  poimirlem23  37644  poimirlem32  37653  itg2addnclem  37672  orfa1  38086  orfa2  38087  inex3  38327  inxpex  38328  mopickr  38352  disjlem14  38797  elpadd0  39810  aks6d1c2p2  42114  sbor2  42207  sn-0ne2  42401  sn-0lt1  42470  hbtlem5  43124  omabs2  43328  safesnsupfiss  43411  safesnsupfidom1o  43413  safesnsupfilb  43414  rp-fakeimass  43508  rp-isfinite6  43514  pr2cv  43544  iunrelexp0  43698  relexpss1d  43701  relexpmulg  43706  iunrelexpmin2  43708  relexp01min  43709  relexp0a  43712  relexpxpmin  43713  relexpaddss  43714  clsk1indlem3  44039  ssrecnpr  44304  seff  44305  sblpnf  44306  expgrowthi  44329  dvconstbi  44330  19.33-2  44378  ax6e2ndeq  44556  en3lpVD  44841  undif3VD  44878  ax6e2ndeqVD  44905  ax6e2ndeqALT  44927  iooinlbub  45506  elprneb  47034  euoreqb  47114  2reu3  47115  afvpcfv0  47151  afvfv0bi  47157  afvco2  47181  afv2orxorb  47233  afv2ndeffv0  47265  afv2fv0b  47271  fvmptrabdm  47298  2ltceilhalf  47333  ceilhalfnn  47341  minusmodnep2tmod  47358  iccpartltu  47430  iccpartgtl  47431  iccpartgt  47432  iccpartleu  47433  iccpartgel  47434  iccpartnel  47443  elsprel  47480  prsprel  47492  sprsymrelfolem2  47498  paireqne  47516  odz2prm2pw  47568  fmtnofac1  47575  fmtno4prmfac  47577  31prm  47602  lighneallem2  47611  lighneallem3  47612  lighneallem4b  47614  lighneallem4  47615  zeo2ALTV  47676  nn0o1gt2ALTV  47699  nn0oALTV  47701  stgoldbwt  47781  sbgoldbwt  47782  sbgoldbalt  47786  sbgoldbm  47789  sbgoldbo  47792  nnsum3primesle9  47799  nnsum4primeseven  47805  nnsum4primesevenALTV  47806  wtgoldbnnsum4prm  47807  bgoldbnnsum3prm  47809  bgoldbtbndlem1  47810  bgoldbtbnd  47814  tgoldbach  47822  vopnbgrelself  47859  clnbgrgrim  47938  grtriproplem  47942  grtrif1o  47945  grtriclwlk3  47948  gpgedgvtx0  48056  gpgcubic  48074  gpg5nbgr3star  48076  gpgprismgr4cycllem3  48091  gpgprismgr4cycllem7  48095  gpgprismgr4cycllem10  48098  pgnbgreunbgrlem3  48112  pgnbgreunbgrlem6  48118  pgnbgreunbgr  48119  upgrwlkupwlk  48132  ztprmneprm  48339  islinindfis  48442  lindslinindsimp2lem5  48455  lindslinindsimp2  48456  lindsrng01  48461  elfzolborelfzop1  48512  flnn0div2ge  48526  blennn0elnn  48570  blen1b  48581  nnolog2flm1  48583  blengt1fldiv2p1  48586  0dig2pr01  48603  dignn0flhalf  48611  nn0sumshdiglemB  48613  nn0sumshdiglem1  48614  resum2sqorgt0  48702  rrx2xpref1o  48711  rrx2plord2  48715  itsclc0yqsol  48757  mosssn  48807  mo0sn  48808  mofsssn  48838  mofmo  48839  f1omo  48885  f1omoOLD  48886