Theorem jaoi 871

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  jao1i  872  jaod  873  pm1.4  883  pm3.2ni  894  pm1.2  917  pm2.4  920  pm2.41  921  orim12i  922  pm1.5  933  pm2.42  957  jaoa  970  jaoian  971  pm4.44  1012  andi  1025  ecase3  1048  cases2ALT  1064  consensus  1068  jaoi3  1076  1fpid3  1098  19.33  1917  19.33b  1918  nfim1  2236  dfsb2  2523  mooran1  2581  eueq3  3669  sbcor  3789  sspss  4050  sspsstr  4057  elun  4100  ssun  4141  inss  4194  raaan2  4478  ifbi  4505  ifcomnan  4539  rabsnifsb  4683  tpprceq3  4767  tppreqb  4768  pwpw0  4774  sssn  4787  snsssn  4801  preq12b  4810  prnebg  4816  preq12nebg  4823  elpr2elpr  4829  prproe  4865  3elpr2eq  4866  unissint  4932  zfpair  5383  axprg  5395  propeqop  5479  propssopi  5480  opthhausdorff  5490  opthhausdorff0  5491  iunopeqop  5494  iunopeqopOLD  5495  relsnb  5780  iresn0n0  6046  sotri2  6123  sotri3  6124  somincom  6128  ordssun  6466  unizlim  6486  onxpdisj  6489  tpres  7205  sorpssuni  7746  ordeleqon  7794  ordunisuc  7841  orduninsuc  7852  tfinds  7869  limomss  7880  limom  7891  soxp  8139  ressuppssdif  8195  tfr2b  8397  omopthi  8663  domnsym  9115  ordfin  9224  brwdom  9554  cantnfvalf  9659  ttrclselem1  9719  elhf2  9903  djuss  9994  djuunxp  9995  eldju2ndl  9998  eldju2ndr  9999  djuun  10000  updjud  10008  iscard3  10165  cflim2  10334  sornom  10348  isfin5  10370  isfin6  10371  sdom2en01  10373  fin23lem29  10412  fin23lem30  10413  fin56  10464  fin67  10466  hsmexlem9  10496  axcc4dom  10512  axdc3lem2  10522  axdc3lem4  10524  brdom3  10600  winainflem  10771  r1tskina  10860  indpi  10985  ltxrlt  11373  nn0sub  12649  nn0n0n1ge2b  12668  nn0ge2m1nn  12669  xnn0xr  12677  xnn0nemnf  12683  elnn0z  12699  nn0lt10b  12754  nn0le2is012  12756  nn0ind-raph  12792  uzin  12994  indstr2  13047  nn0ledivnn  13228  xrnemnf  13239  xrnepnf  13240  mnfltxr  13249  xnn0n0n1ge2b  13254  xnn0ge0  13256  xnn0xaddcl  13358  xnn0lenn0nn0  13368  xnn0xadd0  13370  xmullem2  13388  rexmul  13394  xnn0xrge0  13630  elfzonlteqm1  13869  elfznelfzo  13901  injresinjlem  13918  injresinj  13919  fldiv4p1lem1div2  13968  fldiv4lem1div2  13970  modfzo0difsn  14079  ssnn0fi  14121  fsuppmapnn0fiubex  14128  m1expcl2  14221  m1expeven  14245  zzlesq  14343  sq01  14362  expnngt1  14378  nn0opthi  14407  facp1  14415  faclbnd3  14429  faclbnd4lem1  14430  faclbnd4lem3  14432  bcn1  14450  hashnemnf  14481  hashv01gt1  14482  hashneq0  14501  hashrabrsn  14509  hashrabsn01  14510  hashrabsn1  14511  hashunx  14523  hashsnle1  14555  hashfzp1  14569  hash2pwpr  14614  hashge2el2difr  14619  swrdnd2  14798  pfxnd0  14831  repswswrd  14928  relexpsucl  15177  relexpsucr  15178  relexpcnv  15181  relexprelg  15184  relexpdmg  15188  relexprng  15192  relexpfld  15195  relexpaddg  15199  sumz  15881  arisum  16022  arisum2  16023  pwdif  16030  ntrivcvg  16059  prod1  16104  fprodfac  16133  mod2eq1n2dvds  16510  mulsucdiv2z  16516  nn0o1gt2  16544  nno  16545  nn0o  16546  sumeven  16550  sumodd  16551  divalglem1  16557  divalglem6  16561  gcdaddmlem  16689  dfgcd2  16712  mulgcd  16714  lcmf  16801  lcmfunsnlem2lem2  16807  lcmfunsnlem2  16808  prm2orodd  16859  dfphi2  16944  nnnn0modprm0  16977  prm23lt5  16985  oddprmdvds  17074  4sqlem19  17134  ramz  17196  prmolefac  17217  prmgaplem7  17228  cshwshashlem1  17266  ressval3d  17417  firest  17596  xpsfeq  17728  funcres2c  18071  ex-chn2  18805  smndex1basss  19097  smndex1mgm  19099  smndex1mndlem  19101  mulgnn0gsum  19283  symgfix2  19623  pmtrprfval  19694  m1expaddsub  19705  psgnprfval  19728  gsumpr  20162  gsumzunsnd  20163  0ringnnzr  20769  isfieldidl  21533  frgpcyg  21872  cnmsgnsubg  21876  psgninv  21881  zrhpsgnelbas  21893  m2detleiblem1  22932  symgmatr01lem  22961  indiscld  23402  pnfnei  23531  mnfnei  23532  alexsubALTlem2  24360  alexsubALTlem3  24361  dscmet  24884  xrtgioo  25119  ishl2  25684  iunmbl2  25871  icombl  25878  ioombl  25879  recnprss  26217  recnperf  26218  dvexp2  26267  dvexp3  26291  dvne0f1  26325  plypf1  26524  taylfvallem1  26677  taylfval  26679  tayl0  26682  coseq0negpitopi  26825  logfac  26922  cxpexp  26989  pythag  27138  reasinsin  27217  harmonicbnd3  27328  lgslem4  27620  gausslemma2dlem0i  27684  lgsquadlem2  27701  2lgslem3  27724  2lgs  27727  2lgsoddprmlem3  27734  2sqnn0  27758  2sqnn  27759  ltsres  28012  nolesgn2o  28021  nogesgn1o  28023  nosep1o  28031  nosep2o  28032  noetalem2  28092  sltsun1  28167  sltsun2  28168  eln0s  28740  n0zs  28768  bdaypw2n0bndlem  28842  bdaypw2n0bnd  28843  lfgrnloop  29696  uhgr2edg  29782  usgredg4  29791  usgredg2v  29801  usgrexmplef  29833  nb3grprlem1  29954  uvtx01vtx  29971  wlk1walk  30212  upgriswlk  30214  pthdadjvtx  30306  upgrwlkdvdelem  30315  pthdlem2lem  30346  pthspthcyc  30384  2pthon3v  30525  clwwlkn  30610  clwwlkneq0  30613  eupth2lem3lem4  30825  konigsberg  30851  3vfriswmgrlem  30871  1to2vfriswmgr  30873  1to3vfriswmgr  30874  frgrregorufr0  30918  numclwlk1  30965  ex-pr  31024  shunssi  31963  cvmdi  32919  1neg1t1neg1  33323  iundisj2cnt  33384  fz1nnct  33386  xrge0iifiso  34560  esumpr2  34692  measiuns  34843  sxbrsigalem0  34896  bnj964  35566  subfacval3  35933  kur14lem7  35956  satfrnmapom  36114  gonar  36139  goalr  36141  mrsubcv  36254  nepss  36462  nnuni  36471  fz0n  36475  bccolsum  36483  dfon2lem7  36531  altopthsn  36706  nn0prpw  37091  dissym1  37189  ordcmp  37215  ttciunun  37279  bj-currypeirce  37406  bj-jaoi1  37421  bj-jaoi2  37422  bj-ififc  37432  bj-andnotim  37438  bj-nfimexal  37488  bj-sbsb  37729  bj-elsn12g  37955  bj-ideqg1  38065  finxpreclem2  38293  wl-equsal1i  38456  tan2h  38515  poimirlem23  38541  poimirlem32  38550  itg2addnclem  38569  dfprop1  38625  orfa1  38999  orfa2  39000  inex3  39250  inxpex  39251  mopickr  39283  disjlem14  39813  elpadd0  40846  aks6d1c2p2  43149  quadfac  43235  sbor2  43244  sn-0ne2  43437  sn-0lt1  43519  hbtlem5  44114  omabs2  44318  safesnsupfiss  44400  safesnsupfidom1o  44402  safesnsupfilb  44403  rp-fakeimass  44497  rp-isfinite6  44503  pr2cv  44533  iunrelexp0  44687  relexpss1d  44690  relexpmulg  44695  iunrelexpmin2  44697  relexp01min  44698  relexp0a  44701  relexpxpmin  44702  relexpaddss  44703  clsk1indlem3  45028  ssrecnpr  45277  seff  45278  sblpnf  45279  expgrowthi  45302  dvconstbi  45303  19.33-2  45351  ax6e2ndeq  45527  en3lpVD  45812  undif3VD  45849  ax6e2ndeqVD  45876  ax6e2ndeqALT  45898  iooinlbub  46482  wrddun  47868  chndun  47873  chnrun  47878  elprneb  48068  euoreqb  48148  2reu3  48149  afvpcfv0  48185  afvfv0bi  48191  afvco2  48215  afv2orxorb  48267  afv2ndeffv0  48299  afv2fv0b  48305  fvmptrabdm  48332  nnmul2  48369  2ltceilhalf  48371  ceilhalfnn  48379  minusmodnep2tmod  48398  iccpartltu  48476  iccpartgtl  48477  iccpartgt  48478  iccpartleu  48479  iccpartgel  48480  iccpartnel  48489  elsprel  48526  prsprel  48538  sprsymrelfolem2  48544  paireqne  48562  odz2prm2pw  48617  fmtnofac1  48624  fmtno4prmfac  48626  31prm  48651  lighneallem2  48660  lighneallem3  48661  lighneallem4b  48663  lighneallem4  48664  ppivalnnnprm  48682  ppivalnn  48686  zeo2ALTV  48738  nn0o1gt2ALTV  48761  nn0oALTV  48763  stgoldbwt  48843  sbgoldbwt  48844  sbgoldbalt  48848  sbgoldbm  48851  sbgoldbo  48854  nnsum3primesle9  48861  nnsum4primeseven  48867  nnsum4primesevenALTV  48868  wtgoldbnnsum4prm  48869  bgoldbnnsum3prm  48871  bgoldbtbndlem1  48872  bgoldbtbnd  48876  tgoldbach  48884  vopnbgrelself  48922  clnbgrgrim  49001  grtriproplem  49006  grtrif1o  49009  grtriclwlk3  49012  gpgedgvtx0  49128  gpgcubic  49146  gpg5nbgr3star  49148  gpgprismgr4cycllem3  49164  gpgprismgr4cycllem7  49168  gpgprismgr4cycllem10  49171  pgnbgreunbgrlem3  49185  pgnbgreunbgrlem6  49191  pgnbgreunbgr  49192  upgrwlkupwlk  49207  ztprmneprm  49428  islinindfis  49530  lindslinindsimp2lem5  49543  lindslinindsimp2  49544  lindsrng01  49549  elfzolborelfzop1  49600  flnn0div2ge  49614  blennn0elnn  49658  blen1b  49669  nnolog2flm1  49671  blengt1fldiv2p1  49674  0dig2pr01  49691  dignn0flhalf  49699  nn0sumshdiglemB  49701  nn0sumshdiglem1  49702  resum2sqorgt0  49790  rrx2xpref1o  49799  rrx2plord2  49803  itsclc0yqsol  49845  mosssn  49894  mo0sn  49895  mofsssn  49925  mofmo  49926  f1omo  49970  f1omoOLD  49971