Theorem jaoi 868

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 862	. . 3 ⊢ ((𝜑 ∨ 𝜒) → (¬ 𝜑 → 𝜒))
2		jaoi.2	. . 3 ⊢ (𝜒 → 𝜓)
3	1, 2	syl6 35	. 2 ⊢ ((𝜑 ∨ 𝜒) → (¬ 𝜑 → 𝜓))
4		jaoi.1	. 2 ⊢ (𝜑 → 𝜓)
5	3, 4	pm2.61d2 182	1 ⊢ ((𝜑 ∨ 𝜒) → 𝜓)

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

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 209  df-or 859

This theorem is referenced by:  jao1i  869  jaod  870  pm1.4  880  pm3.2ni  891  pm1.2  914  pm2.4  917  pm2.41  918  orim12i  919  pm1.5  930  pm2.42  955  jaoa  968  jaoian  969  pm4.44  1010  andi  1021  ecase3  1044  cases2ALT  1060  consensus  1064  jaoi3  1072  1fpid3  1093  19.33  1904  19.33b  1905  nfim1  2234  dfsb2  2524  mooran1  2582  eueq3  3674  sbcor  3794  sspss  4055  sspsstr  4062  elun  4106  ssun  4147  inss  4200  raaan2  4476  ifbi  4503  ifcomnan  4537  rabsnifsb  4681  tpprceq3  4764  tppreqb  4765  pwpw0  4771  sssn  4784  snsssn  4799  preq12b  4808  prnebg  4814  preq12nebg  4821  elpr2elpr  4827  prproe  4863  3elpr2eq  4864  unissint  4930  zfpair  5378  axprg  5394  propeqop  5476  propssopi  5477  opthhausdorff  5486  opthhausdorff0  5487  iunopeqop  5490  iunopeqopOLD  5491  relsnb  5775  iresn0n0  6043  sotri2  6116  sotri3  6117  somincom  6121  ordssun  6450  unizlim  6470  onxpdisj  6473  tpres  7185  sorpssuni  7715  ordeleqon  7765  ordunisuc  7812  orduninsuc  7823  tfinds  7840  limomss  7851  limom  7862  soxp  8109  ressuppssdif  8165  tfr2b  8367  omopthi  8631  domnsym  9075  ordfin  9184  brwdom  9515  cantnfvalf  9620  ttrclselem1  9680  djuss  9878  djuunxp  9879  eldju2ndl  9882  eldju2ndr  9883  djuun  9884  updjud  9892  iscard3  10049  cflim2  10220  sornom  10234  isfin5  10256  isfin6  10257  sdom2en01  10259  fin23lem29  10298  fin23lem30  10299  fin56  10350  fin67  10352  hsmexlem9  10382  axcc4dom  10398  axdc3lem2  10408  axdc3lem4  10410  brdom3  10485  winainflem  10651  r1tskina  10740  indpi  10865  ltxrlt  11253  nn0sub  12531  nn0n0n1ge2b  12550  nn0ge2m1nn  12551  xnn0xr  12559  xnn0nemnf  12565  elnn0z  12581  nn0lt10b  12635  nn0le2is012  12637  nn0ind-raph  12673  uzin  12875  indstr2  12928  nn0ledivnn  13108  xrnemnf  13119  xrnepnf  13120  mnfltxr  13129  xnn0n0n1ge2b  13134  xnn0ge0  13136  xnn0xaddcl  13238  xnn0lenn0nn0  13248  xnn0xadd0  13250  xmullem2  13268  rexmul  13274  xnn0xrge0  13510  elfzonlteqm1  13747  elfznelfzo  13779  injresinjlem  13796  injresinj  13797  fldiv4p1lem1div2  13845  fldiv4lem1div2  13847  modfzo0difsn  13956  ssnn0fi  13998  fsuppmapnn0fiubex  14005  m1expcl2  14098  m1expeven  14122  zzlesq  14219  sq01  14238  expnngt1  14254  nn0opthi  14283  facp1  14291  faclbnd3  14305  faclbnd4lem1  14306  faclbnd4lem3  14308  bcn1  14326  hashnemnf  14357  hashv01gt1  14358  hashneq0  14377  hashrabrsn  14385  hashrabsn01  14386  hashrabsn1  14387  hashunx  14399  hashsnle1  14430  hashfzp1  14444  hash2pwpr  14489  hashge2el2difr  14494  swrdnd2  14669  pfxnd0  14702  repswswrd  14797  relexpsucl  15044  relexpsucr  15045  relexpcnv  15048  relexprelg  15051  relexpdmg  15055  relexprng  15059  relexpfld  15062  relexpaddg  15066  sumz  15749  arisum  15890  arisum2  15891  pwdif  15898  ntrivcvg  15927  prod1  15974  fprodfac  16003  mod2eq1n2dvds  16381  mulsucdiv2z  16387  nn0o1gt2  16415  nno  16416  nn0o  16417  sumeven  16421  sumodd  16422  divalglem1  16428  divalglem6  16432  gcdaddmlem  16558  dfgcd2  16580  mulgcd  16582  lcmf  16667  lcmfunsnlem2lem2  16673  lcmfunsnlem2  16674  prm2orodd  16725  dfphi2  16809  nnnn0modprm0  16842  prm23lt5  16850  oddprmdvds  16939  4sqlem19  16999  ramz  17061  prmolefac  17082  prmgaplem7  17093  cshwshashlem1  17131  ressval3d  17282  firest  17461  xpsfeq  17593  funcres2c  17936  ex-chn2  18670  smndex1basss  18942  smndex1mgm  18944  smndex1mndlem  18946  mulgnn0gsum  19122  symgfix2  19456  pmtrprfval  19527  m1expaddsub  19538  psgnprfval  19561  gsumpr  19995  gsumzunsnd  19996  0ringnnzr  20571  frgpcyg  21622  cnmsgnsubg  21626  psgninv  21631  zrhpsgnelbas  21643  m2detleiblem1  22681  symgmatr01lem  22710  indiscld  23148  pnfnei  23277  mnfnei  23278  alexsubALTlem2  24105  alexsubALTlem3  24106  dscmet  24629  xrtgioo  24864  ishl2  25429  iunmbl2  25616  icombl  25623  ioombl  25624  recnprss  25963  recnperf  25964  dvexp2  26013  dvexp3  26037  dvne0f1  26071  plypf1  26269  taylfvallem1  26417  taylfval  26419  tayl0  26422  coseq0negpitopi  26565  logfac  26663  cxpexp  26730  pythag  26879  reasinsin  26958  harmonicbnd3  27069  lgslem4  27361  gausslemma2dlem0i  27425  lgsquadlem2  27442  2lgslem3  27465  2lgs  27468  2lgsoddprmlem3  27475  2sqnn0  27499  2sqnn  27500  ltsres  27723  nolesgn2o  27732  nogesgn1o  27734  nosep1o  27742  nosep2o  27743  noetalem2  27803  sltsun1  27878  sltsun2  27879  eln0s  28451  n0zs  28479  bdaypw2n0bndlem  28553  bdaypw2n0bnd  28554  lfgrnloop  29323  uhgr2edg  29406  usgredg4  29415  usgredg2v  29425  usgrexmplef  29457  nb3grprlem1  29578  uvtx01vtx  29595  wlk1walk  29836  upgriswlk  29838  pthdadjvtx  29925  upgrwlkdvdelem  29933  pthdlem2lem  29964  pthspthcyc  30000  2pthon3v  30140  clwwlkn  30225  clwwlkneq0  30228  eupth2lem3lem4  30430  konigsberg  30456  3vfriswmgrlem  30476  1to2vfriswmgr  30478  1to3vfriswmgr  30479  frgrregorufr0  30523  numclwlk1  30570  ex-pr  30629  shunssi  31568  cvmdi  32524  1neg1t1neg1  32937  iundisj2cnt  32998  fz1nnct  33000  xrge0iifiso  34229  esumpr2  34361  measiuns  34511  sxbrsigalem0  34565  bnj964  35235  subfacval3  35536  kur14lem7  35559  satfrnmapom  35717  gonar  35742  goalr  35744  mrsubcv  35857  nepss  36065  nnuni  36074  fz0n  36078  bccolsum  36086  dfon2lem7  36134  altopthsn  36308  elhf2  36522  nn0prpw  36680  dissym1  36778  ordcmp  36804  ttciunun  36868  bj-currypeirce  36996  bj-jaoi1  37011  bj-jaoi2  37012  bj-ififc  37022  bj-andnotim  37028  bj-nfimexal  37078  bj-sbsb  37319  bj-elsn12g  37542  bj-ideqg1  37653  finxpreclem2  37881  wl-equsal1i  38044  tan2h  38108  poimirlem23  38139  poimirlem32  38148  itg2addnclem  38167  orfa1  38581  orfa2  38582  inex3  38834  inxpex  38835  mopickr  38867  disjlem14  39397  elpadd0  40430  aks6d1c2p2  42733  sbor2  42826  sn-0ne2  43012  sn-0lt1  43094  hbtlem5  43702  omabs2  43906  safesnsupfiss  43988  safesnsupfidom1o  43990  safesnsupfilb  43991  rp-fakeimass  44085  rp-isfinite6  44091  pr2cv  44121  iunrelexp0  44275  relexpss1d  44278  relexpmulg  44283  iunrelexpmin2  44285  relexp01min  44286  relexp0a  44289  relexpxpmin  44290  relexpaddss  44291  clsk1indlem3  44616  ssrecnpr  44881  seff  44882  sblpnf  44883  expgrowthi  44906  dvconstbi  44907  19.33-2  44955  ax6e2ndeq  45132  en3lpVD  45417  undif3VD  45454  ax6e2ndeqVD  45481  ax6e2ndeqALT  45503  iooinlbub  46074  elprneb  47620  euoreqb  47700  2reu3  47701  afvpcfv0  47737  afvfv0bi  47743  afvco2  47767  afv2orxorb  47819  afv2ndeffv0  47851  afv2fv0b  47857  fvmptrabdm  47884  nnmul2  47921  2ltceilhalf  47923  ceilhalfnn  47931  minusmodnep2tmod  47950  iccpartltu  48028  iccpartgtl  48029  iccpartgt  48030  iccpartleu  48031  iccpartgel  48032  iccpartnel  48041  elsprel  48078  prsprel  48090  sprsymrelfolem2  48096  paireqne  48114  odz2prm2pw  48169  fmtnofac1  48176  fmtno4prmfac  48178  31prm  48203  lighneallem2  48212  lighneallem3  48213  lighneallem4b  48215  lighneallem4  48216  ppivalnnnprm  48234  ppivalnn  48238  zeo2ALTV  48290  nn0o1gt2ALTV  48313  nn0oALTV  48315  stgoldbwt  48395  sbgoldbwt  48396  sbgoldbalt  48400  sbgoldbm  48403  sbgoldbo  48406  nnsum3primesle9  48413  nnsum4primeseven  48419  nnsum4primesevenALTV  48420  wtgoldbnnsum4prm  48421  bgoldbnnsum3prm  48423  bgoldbtbndlem1  48424  bgoldbtbnd  48428  tgoldbach  48436  vopnbgrelself  48474  clnbgrgrim  48553  grtriproplem  48558  grtrif1o  48561  grtriclwlk3  48564  gpgedgvtx0  48680  gpgcubic  48698  gpg5nbgr3star  48700  gpgprismgr4cycllem3  48716  gpgprismgr4cycllem7  48720  gpgprismgr4cycllem10  48723  pgnbgreunbgrlem3  48737  pgnbgreunbgrlem6  48743  pgnbgreunbgr  48744  upgrwlkupwlk  48759  ztprmneprm  48966  islinindfis  49068  lindslinindsimp2lem5  49081  lindslinindsimp2  49082  lindsrng01  49087  elfzolborelfzop1  49138  flnn0div2ge  49152  blennn0elnn  49196  blen1b  49207  nnolog2flm1  49209  blengt1fldiv2p1  49212  0dig2pr01  49229  dignn0flhalf  49237  nn0sumshdiglemB  49239  nn0sumshdiglem1  49240  resum2sqorgt0  49328  rrx2xpref1o  49337  rrx2plord2  49341  itsclc0yqsol  49383  mosssn  49433  mo0sn  49434  mofsssn  49464  mofmo  49465  f1omo  49511  f1omoOLD  49512