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  2237  dfsb2  2524  mooran1  2582  eueq3  3672  sbcor  3792  sspss  4053  sspsstr  4060  elun  4103  ssun  4144  inss  4197  raaan2  4481  ifbi  4508  ifcomnan  4542  rabsnifsb  4686  tpprceq3  4770  tppreqb  4771  pwpw0  4777  sssn  4790  snsssn  4804  preq12b  4813  prnebg  4819  preq12nebg  4826  elpr2elpr  4832  prproe  4868  3elpr2eq  4869  unissint  4935  zfpair  5390  axprg  5406  propeqop  5488  propssopi  5489  opthhausdorff  5498  opthhausdorff0  5499  iunopeqop  5502  iunopeqopOLD  5503  relsnb  5787  iresn0n0  6054  sotri2  6127  sotri3  6128  somincom  6132  ordssun  6466  unizlim  6486  onxpdisj  6489  tpres  7203  sorpssuni  7736  ordeleqon  7784  ordunisuc  7831  orduninsuc  7842  tfinds  7859  limomss  7870  limom  7881  soxp  8130  ressuppssdif  8186  tfr2b  8388  omopthi  8652  domnsym  9104  ordfin  9213  brwdom  9542  cantnfvalf  9647  ttrclselem1  9707  djuss  9928  djuunxp  9929  eldju2ndl  9932  eldju2ndr  9933  djuun  9934  updjud  9942  iscard3  10099  cflim2  10268  sornom  10282  isfin5  10304  isfin6  10305  sdom2en01  10307  fin23lem29  10346  fin23lem30  10347  fin56  10398  fin67  10400  hsmexlem9  10430  axcc4dom  10446  axdc3lem2  10456  axdc3lem4  10458  brdom3  10534  winainflem  10705  r1tskina  10794  indpi  10919  ltxrlt  11307  nn0sub  12581  nn0n0n1ge2b  12600  nn0ge2m1nn  12601  xnn0xr  12609  xnn0nemnf  12615  elnn0z  12631  nn0lt10b  12686  nn0le2is012  12688  nn0ind-raph  12724  uzin  12926  indstr2  12979  nn0ledivnn  13159  xrnemnf  13170  xrnepnf  13171  mnfltxr  13180  xnn0n0n1ge2b  13185  xnn0ge0  13187  xnn0xaddcl  13289  xnn0lenn0nn0  13299  xnn0xadd0  13301  xmullem2  13319  rexmul  13325  xnn0xrge0  13561  elfzonlteqm1  13799  elfznelfzo  13831  injresinjlem  13848  injresinj  13849  fldiv4p1lem1div2  13898  fldiv4lem1div2  13900  modfzo0difsn  14009  ssnn0fi  14051  fsuppmapnn0fiubex  14058  m1expcl2  14151  m1expeven  14175  zzlesq  14272  sq01  14291  expnngt1  14307  nn0opthi  14336  facp1  14344  faclbnd3  14358  faclbnd4lem1  14359  faclbnd4lem3  14361  bcn1  14379  hashnemnf  14410  hashv01gt1  14411  hashneq0  14430  hashrabrsn  14438  hashrabsn01  14439  hashrabsn1  14440  hashunx  14452  hashsnle1  14484  hashfzp1  14498  hash2pwpr  14543  hashge2el2difr  14548  swrdnd2  14727  pfxnd0  14760  repswswrd  14857  relexpsucl  15106  relexpsucr  15107  relexpcnv  15110  relexprelg  15113  relexpdmg  15117  relexprng  15121  relexpfld  15124  relexpaddg  15128  sumz  15810  arisum  15951  arisum2  15952  pwdif  15959  ntrivcvg  15988  prod1  16035  fprodfac  16064  mod2eq1n2dvds  16441  mulsucdiv2z  16447  nn0o1gt2  16475  nno  16476  nn0o  16477  sumeven  16481  sumodd  16482  divalglem1  16488  divalglem6  16492  gcdaddmlem  16618  dfgcd2  16640  mulgcd  16642  lcmf  16727  lcmfunsnlem2lem2  16733  lcmfunsnlem2  16734  prm2orodd  16785  dfphi2  16869  nnnn0modprm0  16902  prm23lt5  16910  oddprmdvds  16999  4sqlem19  17059  ramz  17121  prmolefac  17142  prmgaplem7  17153  cshwshashlem1  17191  ressval3d  17342  firest  17521  xpsfeq  17653  funcres2c  17996  ex-chn2  18730  smndex1basss  19018  smndex1mgm  19020  smndex1mndlem  19022  mulgnn0gsum  19204  symgfix2  19544  pmtrprfval  19615  m1expaddsub  19626  psgnprfval  19649  gsumpr  20083  gsumzunsnd  20084  0ringnnzr  20687  isfieldidl  21450  frgpcyg  21787  cnmsgnsubg  21791  psgninv  21796  zrhpsgnelbas  21808  m2detleiblem1  22847  symgmatr01lem  22876  indiscld  23317  pnfnei  23446  mnfnei  23447  alexsubALTlem2  24275  alexsubALTlem3  24276  dscmet  24799  xrtgioo  25034  ishl2  25599  iunmbl2  25786  icombl  25793  ioombl  25794  recnprss  26133  recnperf  26134  dvexp2  26183  dvexp3  26207  dvne0f1  26241  plypf1  26439  taylfvallem1  26590  taylfval  26592  tayl0  26595  coseq0negpitopi  26738  logfac  26836  cxpexp  26903  pythag  27052  reasinsin  27131  harmonicbnd3  27242  lgslem4  27534  gausslemma2dlem0i  27598  lgsquadlem2  27615  2lgslem3  27638  2lgs  27641  2lgsoddprmlem3  27648  2sqnn0  27672  2sqnn  27673  ltsres  27896  nolesgn2o  27905  nogesgn1o  27907  nosep1o  27915  nosep2o  27916  noetalem2  27976  sltsun1  28051  sltsun2  28052  eln0s  28624  n0zs  28652  bdaypw2n0bndlem  28726  bdaypw2n0bnd  28727  lfgrnloop  29568  uhgr2edg  29654  usgredg4  29663  usgredg2v  29673  usgrexmplef  29705  nb3grprlem1  29826  uvtx01vtx  29843  wlk1walk  30084  upgriswlk  30086  pthdadjvtx  30178  upgrwlkdvdelem  30187  pthdlem2lem  30218  pthspthcyc  30256  2pthon3v  30397  clwwlkn  30482  clwwlkneq0  30485  eupth2lem3lem4  30697  konigsberg  30723  3vfriswmgrlem  30743  1to2vfriswmgr  30745  1to3vfriswmgr  30746  frgrregorufr0  30790  numclwlk1  30837  ex-pr  30896  shunssi  31835  cvmdi  32791  1neg1t1neg1  33196  iundisj2cnt  33257  fz1nnct  33259  xrge0iifiso  34432  esumpr2  34564  measiuns  34715  sxbrsigalem0  34769  bnj964  35439  subfacval3  35755  kur14lem7  35778  satfrnmapom  35936  gonar  35961  goalr  35963  mrsubcv  36076  nepss  36284  nnuni  36293  fz0n  36297  bccolsum  36305  dfon2lem7  36353  altopthsn  36528  elhf2  36742  nn0prpw  36929  dissym1  37027  ordcmp  37053  ttciunun  37117  bj-currypeirce  37244  bj-jaoi1  37259  bj-jaoi2  37260  bj-ififc  37270  bj-andnotim  37276  bj-nfimexal  37326  bj-sbsb  37567  bj-elsn12g  37791  bj-ideqg1  37903  finxpreclem2  38131  wl-equsal1i  38294  tan2h  38353  poimirlem23  38379  poimirlem32  38388  itg2addnclem  38407  orfa1  38822  orfa2  38823  inex3  39073  inxpex  39074  mopickr  39106  disjlem14  39636  elpadd0  40669  aks6d1c2p2  42972  quadfac  43058  sbor2  43067  sn-0ne2  43268  sn-0lt1  43350  hbtlem5  43956  omabs2  44160  safesnsupfiss  44242  safesnsupfidom1o  44244  safesnsupfilb  44245  rp-fakeimass  44339  rp-isfinite6  44345  pr2cv  44375  iunrelexp0  44529  relexpss1d  44532  relexpmulg  44537  iunrelexpmin2  44539  relexp01min  44540  relexp0a  44543  relexpxpmin  44544  relexpaddss  44545  clsk1indlem3  44870  ssrecnpr  45119  seff  45120  sblpnf  45121  expgrowthi  45144  dvconstbi  45145  19.33-2  45193  ax6e2ndeq  45369  en3lpVD  45654  undif3VD  45691  ax6e2ndeqVD  45718  ax6e2ndeqALT  45740  iooinlbub  46318  wrddun  47704  chndun  47709  chnrun  47714  elprneb  47904  euoreqb  47984  2reu3  47985  afvpcfv0  48021  afvfv0bi  48027  afvco2  48051  afv2orxorb  48103  afv2ndeffv0  48135  afv2fv0b  48141  fvmptrabdm  48168  nnmul2  48205  2ltceilhalf  48207  ceilhalfnn  48215  minusmodnep2tmod  48234  iccpartltu  48312  iccpartgtl  48313  iccpartgt  48314  iccpartleu  48315  iccpartgel  48316  iccpartnel  48325  elsprel  48362  prsprel  48374  sprsymrelfolem2  48380  paireqne  48398  odz2prm2pw  48453  fmtnofac1  48460  fmtno4prmfac  48462  31prm  48487  lighneallem2  48496  lighneallem3  48497  lighneallem4b  48499  lighneallem4  48500  ppivalnnnprm  48518  ppivalnn  48522  zeo2ALTV  48574  nn0o1gt2ALTV  48597  nn0oALTV  48599  stgoldbwt  48679  sbgoldbwt  48680  sbgoldbalt  48684  sbgoldbm  48687  sbgoldbo  48690  nnsum3primesle9  48697  nnsum4primeseven  48703  nnsum4primesevenALTV  48704  wtgoldbnnsum4prm  48705  bgoldbnnsum3prm  48707  bgoldbtbndlem1  48708  bgoldbtbnd  48712  tgoldbach  48720  vopnbgrelself  48758  clnbgrgrim  48837  grtriproplem  48842  grtrif1o  48845  grtriclwlk3  48848  gpgedgvtx0  48964  gpgcubic  48982  gpg5nbgr3star  48984  gpgprismgr4cycllem3  49000  gpgprismgr4cycllem7  49004  gpgprismgr4cycllem10  49007  pgnbgreunbgrlem3  49021  pgnbgreunbgrlem6  49027  pgnbgreunbgr  49028  upgrwlkupwlk  49043  ztprmneprm  49264  islinindfis  49366  lindslinindsimp2lem5  49379  lindslinindsimp2  49380  lindsrng01  49385  elfzolborelfzop1  49436  flnn0div2ge  49450  blennn0elnn  49494  blen1b  49505  nnolog2flm1  49507  blengt1fldiv2p1  49510  0dig2pr01  49527  dignn0flhalf  49535  nn0sumshdiglemB  49537  nn0sumshdiglem1  49538  resum2sqorgt0  49626  rrx2xpref1o  49635  rrx2plord2  49639  itsclc0yqsol  49681  mosssn  49730  mo0sn  49731  mofsssn  49761  mofmo  49762  f1omo  49806  f1omoOLD  49807