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  2238  dfsb2  2527  mooran1  2585  eueq3  3676  sbcor  3796  sspss  4057  sspsstr  4064  elun  4107  ssun  4148  inss  4201  raaan2  4485  ifbi  4512  ifcomnan  4546  rabsnifsb  4690  tpprceq3  4774  tppreqb  4775  pwpw0  4781  sssn  4794  snsssn  4808  preq12b  4817  prnebg  4823  preq12nebg  4830  elpr2elpr  4836  prproe  4872  3elpr2eq  4873  unissint  4939  zfpair  5394  axprg  5410  propeqop  5492  propssopi  5493  opthhausdorff  5502  opthhausdorff0  5503  iunopeqop  5506  iunopeqopOLD  5507  relsnb  5791  iresn0n0  6058  sotri2  6131  sotri3  6132  somincom  6136  ordssun  6469  unizlim  6489  onxpdisj  6492  tpres  7206  sorpssuni  7739  ordeleqon  7787  ordunisuc  7834  orduninsuc  7845  tfinds  7862  limomss  7873  limom  7884  soxp  8131  ressuppssdif  8187  tfr2b  8389  omopthi  8653  domnsym  9098  ordfin  9207  brwdom  9536  cantnfvalf  9641  ttrclselem1  9701  djuss  9922  djuunxp  9923  eldju2ndl  9926  eldju2ndr  9927  djuun  9928  updjud  9936  iscard3  10093  cflim2  10262  sornom  10276  isfin5  10298  isfin6  10299  sdom2en01  10301  fin23lem29  10340  fin23lem30  10341  fin56  10392  fin67  10394  hsmexlem9  10424  axcc4dom  10440  axdc3lem2  10450  axdc3lem4  10452  brdom3  10527  winainflem  10693  r1tskina  10782  indpi  10907  ltxrlt  11295  nn0sub  12569  nn0n0n1ge2b  12588  nn0ge2m1nn  12589  xnn0xr  12597  xnn0nemnf  12603  elnn0z  12619  nn0lt10b  12674  nn0le2is012  12676  nn0ind-raph  12712  uzin  12914  indstr2  12967  nn0ledivnn  13147  xrnemnf  13158  xrnepnf  13159  mnfltxr  13168  xnn0n0n1ge2b  13173  xnn0ge0  13175  xnn0xaddcl  13277  xnn0lenn0nn0  13287  xnn0xadd0  13289  xmullem2  13307  rexmul  13313  xnn0xrge0  13549  elfzonlteqm1  13787  elfznelfzo  13819  injresinjlem  13836  injresinj  13837  fldiv4p1lem1div2  13886  fldiv4lem1div2  13888  modfzo0difsn  13997  ssnn0fi  14039  fsuppmapnn0fiubex  14046  m1expcl2  14139  m1expeven  14163  zzlesq  14260  sq01  14279  expnngt1  14295  nn0opthi  14324  facp1  14332  faclbnd3  14346  faclbnd4lem1  14347  faclbnd4lem3  14349  bcn1  14367  hashnemnf  14398  hashv01gt1  14399  hashneq0  14418  hashrabrsn  14426  hashrabsn01  14427  hashrabsn1  14428  hashunx  14440  hashsnle1  14472  hashfzp1  14486  hash2pwpr  14531  hashge2el2difr  14536  swrdnd2  14715  pfxnd0  14748  repswswrd  14845  relexpsucl  15092  relexpsucr  15093  relexpcnv  15096  relexprelg  15099  relexpdmg  15103  relexprng  15107  relexpfld  15110  relexpaddg  15114  sumz  15796  arisum  15937  arisum2  15938  pwdif  15945  ntrivcvg  15974  prod1  16021  fprodfac  16050  mod2eq1n2dvds  16427  mulsucdiv2z  16433  nn0o1gt2  16461  nno  16462  nn0o  16463  sumeven  16467  sumodd  16468  divalglem1  16474  divalglem6  16478  gcdaddmlem  16604  dfgcd2  16626  mulgcd  16628  lcmf  16713  lcmfunsnlem2lem2  16719  lcmfunsnlem2  16720  prm2orodd  16771  dfphi2  16855  nnnn0modprm0  16888  prm23lt5  16896  oddprmdvds  16985  4sqlem19  17045  ramz  17107  prmolefac  17128  prmgaplem7  17139  cshwshashlem1  17177  ressval3d  17328  firest  17507  xpsfeq  17639  funcres2c  17982  ex-chn2  18716  smndex1basss  19004  smndex1mgm  19006  smndex1mndlem  19008  mulgnn0gsum  19190  symgfix2  19530  pmtrprfval  19601  m1expaddsub  19612  psgnprfval  19635  gsumpr  20069  gsumzunsnd  20070  0ringnnzr  20673  isfieldidl  21436  frgpcyg  21773  cnmsgnsubg  21777  psgninv  21782  zrhpsgnelbas  21794  m2detleiblem1  22831  symgmatr01lem  22860  indiscld  23298  pnfnei  23427  mnfnei  23428  alexsubALTlem2  24256  alexsubALTlem3  24257  dscmet  24780  xrtgioo  25015  ishl2  25580  iunmbl2  25767  icombl  25774  ioombl  25775  recnprss  26114  recnperf  26115  dvexp2  26164  dvexp3  26188  dvne0f1  26222  plypf1  26420  taylfvallem1  26571  taylfval  26573  tayl0  26576  coseq0negpitopi  26719  logfac  26817  cxpexp  26884  pythag  27033  reasinsin  27112  harmonicbnd3  27223  lgslem4  27515  gausslemma2dlem0i  27579  lgsquadlem2  27596  2lgslem3  27619  2lgs  27622  2lgsoddprmlem3  27629  2sqnn0  27653  2sqnn  27654  ltsres  27877  nolesgn2o  27886  nogesgn1o  27888  nosep1o  27896  nosep2o  27897  noetalem2  27957  sltsun1  28032  sltsun2  28033  eln0s  28605  n0zs  28633  bdaypw2n0bndlem  28707  bdaypw2n0bnd  28708  lfgrnloop  29530  uhgr2edg  29616  usgredg4  29625  usgredg2v  29635  usgrexmplef  29667  nb3grprlem1  29788  uvtx01vtx  29805  wlk1walk  30046  upgriswlk  30048  pthdadjvtx  30140  upgrwlkdvdelem  30149  pthdlem2lem  30180  pthspthcyc  30218  2pthon3v  30359  clwwlkn  30444  clwwlkneq0  30447  eupth2lem3lem4  30653  konigsberg  30679  3vfriswmgrlem  30699  1to2vfriswmgr  30701  1to3vfriswmgr  30702  frgrregorufr0  30746  numclwlk1  30793  ex-pr  30852  shunssi  31791  cvmdi  32747  1neg1t1neg1  33153  iundisj2cnt  33214  fz1nnct  33216  xrge0iifiso  34389  esumpr2  34521  measiuns  34672  sxbrsigalem0  34726  bnj964  35396  subfacval3  35718  kur14lem7  35741  satfrnmapom  35899  gonar  35924  goalr  35926  mrsubcv  36039  nepss  36247  nnuni  36256  fz0n  36260  bccolsum  36268  dfon2lem7  36316  altopthsn  36490  elhf2  36704  nn0prpw  36891  dissym1  36989  ordcmp  37015  ttciunun  37079  bj-currypeirce  37206  bj-jaoi1  37221  bj-jaoi2  37222  bj-ififc  37232  bj-andnotim  37238  bj-nfimexal  37288  bj-sbsb  37529  bj-elsn12g  37753  bj-ideqg1  37865  finxpreclem2  38093  wl-equsal1i  38256  tan2h  38320  poimirlem23  38351  poimirlem32  38360  itg2addnclem  38379  orfa1  38794  orfa2  38795  inex3  39045  inxpex  39046  mopickr  39078  disjlem14  39608  elpadd0  40641  aks6d1c2p2  42944  quadfac  43030  sbor2  43039  sn-0ne2  43225  sn-0lt1  43307  hbtlem5  43913  omabs2  44117  safesnsupfiss  44199  safesnsupfidom1o  44201  safesnsupfilb  44202  rp-fakeimass  44296  rp-isfinite6  44302  pr2cv  44332  iunrelexp0  44486  relexpss1d  44489  relexpmulg  44494  iunrelexpmin2  44496  relexp01min  44497  relexp0a  44500  relexpxpmin  44501  relexpaddss  44502  clsk1indlem3  44827  ssrecnpr  45076  seff  45077  sblpnf  45078  expgrowthi  45101  dvconstbi  45102  19.33-2  45150  ax6e2ndeq  45326  en3lpVD  45611  undif3VD  45648  ax6e2ndeqVD  45675  ax6e2ndeqALT  45697  iooinlbub  46275  elprneb  47824  euoreqb  47904  2reu3  47905  afvpcfv0  47941  afvfv0bi  47947  afvco2  47971  afv2orxorb  48023  afv2ndeffv0  48055  afv2fv0b  48061  fvmptrabdm  48088  nnmul2  48125  2ltceilhalf  48127  ceilhalfnn  48135  minusmodnep2tmod  48154  iccpartltu  48232  iccpartgtl  48233  iccpartgt  48234  iccpartleu  48235  iccpartgel  48236  iccpartnel  48245  elsprel  48282  prsprel  48294  sprsymrelfolem2  48300  paireqne  48318  odz2prm2pw  48373  fmtnofac1  48380  fmtno4prmfac  48382  31prm  48407  lighneallem2  48416  lighneallem3  48417  lighneallem4b  48419  lighneallem4  48420  ppivalnnnprm  48438  ppivalnn  48442  zeo2ALTV  48494  nn0o1gt2ALTV  48517  nn0oALTV  48519  stgoldbwt  48599  sbgoldbwt  48600  sbgoldbalt  48604  sbgoldbm  48607  sbgoldbo  48610  nnsum3primesle9  48617  nnsum4primeseven  48623  nnsum4primesevenALTV  48624  wtgoldbnnsum4prm  48625  bgoldbnnsum3prm  48627  bgoldbtbndlem1  48628  bgoldbtbnd  48632  tgoldbach  48640  vopnbgrelself  48678  clnbgrgrim  48757  grtriproplem  48762  grtrif1o  48765  grtriclwlk3  48768  gpgedgvtx0  48884  gpgcubic  48902  gpg5nbgr3star  48904  gpgprismgr4cycllem3  48920  gpgprismgr4cycllem7  48924  gpgprismgr4cycllem10  48927  pgnbgreunbgrlem3  48941  pgnbgreunbgrlem6  48947  pgnbgreunbgr  48948  upgrwlkupwlk  48963  ztprmneprm  49184  islinindfis  49286  lindslinindsimp2lem5  49299  lindslinindsimp2  49300  lindsrng01  49305  elfzolborelfzop1  49356  flnn0div2ge  49370  blennn0elnn  49414  blen1b  49425  nnolog2flm1  49427  blengt1fldiv2p1  49430  0dig2pr01  49447  dignn0flhalf  49455  nn0sumshdiglemB  49457  nn0sumshdiglem1  49458  resum2sqorgt0  49546  rrx2xpref1o  49555  rrx2plord2  49559  itsclc0yqsol  49601  mosssn  49650  mo0sn  49651  mofsssn  49681  mofmo  49682  f1omo  49728  f1omoOLD  49729