Theorem jaoi 863

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 857	. . 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 853

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 208  df-or 854

This theorem is referenced by:  jao1i  864  jaod  865  pm1.4  875  pm3.2ni  886  pm1.2  909  pm2.4  912  pm2.41  913  orim12i  914  pm1.5  925  pm2.42  950  jaoa  963  jaoian  964  pm4.44  1004  andi  1015  ecase3  1038  cases2ALT  1054  consensus  1058  jaoi3  1066  1fpid3  1087  19.33  1891  19.33b  1892  nfim1  2211  dfsb2  2501  mooran1  2559  eueq3  3652  sbcor  3773  sspss  4033  sspsstr  4039  elun  4083  ssun  4124  inss  4176  raaan2  4450  ifbi  4477  ifcomnan  4511  rabsnifsb  4654  tpprceq3  4737  tppreqb  4738  pwpw0  4744  sssn  4757  snsssn  4772  preq12b  4781  prnebg  4787  preq12nebg  4794  elpr2elpr  4800  prproe  4836  3elpr2eq  4837  unissint  4902  zfpair  5350  axprg  5366  propeqop  5448  propssopi  5449  opthhausdorff  5458  opthhausdorff0  5459  iunopeqop  5462  iunopeqopOLD  5463  relsnb  5745  iresn0n0  6006  sotri2  6079  sotri3  6080  somincom  6084  ordssun  6414  unizlim  6434  onxpdisj  6437  tpres  7145  sorpssuni  7675  ordeleqon  7725  ordunisuc  7772  orduninsuc  7783  tfinds  7800  limomss  7811  limom  7822  soxp  8069  ressuppssdif  8125  tfr2b  8325  omopthi  8587  domnsym  9031  ordfin  9140  brwdom  9472  cantnfvalf  9577  ttrclselem1  9637  djuss  9835  djuunxp  9836  eldju2ndl  9839  eldju2ndr  9840  djuun  9841  updjud  9849  iscard3  10006  cflim2  10176  sornom  10190  isfin5  10212  isfin6  10213  sdom2en01  10215  fin23lem29  10254  fin23lem30  10255  fin56  10306  fin67  10308  hsmexlem9  10338  axcc4dom  10354  axdc3lem2  10364  axdc3lem4  10366  brdom3  10441  winainflem  10607  r1tskina  10696  indpi  10821  ltxrlt  11207  nn0sub  12478  nn0n0n1ge2b  12497  nn0ge2m1nn  12498  xnn0xr  12506  xnn0nemnf  12512  elnn0z  12528  nn0lt10b  12582  nn0le2is012  12584  nn0ind-raph  12620  uzin  12815  indstr2  12868  nn0ledivnn  13048  xrnemnf  13059  xrnepnf  13060  mnfltxr  13069  xnn0n0n1ge2b  13074  xnn0ge0  13076  xnn0xaddcl  13178  xnn0lenn0nn0  13188  xnn0xadd0  13190  xmullem2  13208  rexmul  13214  xnn0xrge0  13450  elfzonlteqm1  13687  elfznelfzo  13719  injresinjlem  13736  injresinj  13737  fldiv4p1lem1div2  13785  fldiv4lem1div2  13787  modfzo0difsn  13896  ssnn0fi  13938  fsuppmapnn0fiubex  13945  m1expcl2  14038  m1expeven  14062  zzlesq  14159  sq01  14178  expnngt1  14194  nn0opthi  14223  facp1  14231  faclbnd3  14245  faclbnd4lem1  14246  faclbnd4lem3  14248  bcn1  14266  hashnemnf  14297  hashv01gt1  14298  hashneq0  14317  hashrabrsn  14325  hashrabsn01  14326  hashrabsn1  14327  hashunx  14339  hashsnle1  14370  hashfzp1  14384  hash2pwpr  14429  hashge2el2difr  14434  swrdnd2  14609  pfxnd0  14642  repswswrd  14737  relexpsucl  14984  relexpsucr  14985  relexpcnv  14988  relexprelg  14991  relexpdmg  14995  relexprng  14999  relexpfld  15002  relexpaddg  15006  sumz  15675  arisum  15816  arisum2  15817  pwdif  15824  ntrivcvg  15853  prod1  15900  fprodfac  15929  mod2eq1n2dvds  16307  mulsucdiv2z  16313  nn0o1gt2  16341  nno  16342  nn0o  16343  sumeven  16347  sumodd  16348  divalglem1  16354  divalglem6  16358  gcdaddmlem  16484  dfgcd2  16506  mulgcd  16508  lcmf  16593  lcmfunsnlem2lem2  16599  lcmfunsnlem2  16600  prm2orodd  16651  dfphi2  16735  nnnn0modprm0  16768  prm23lt5  16776  oddprmdvds  16865  4sqlem19  16925  ramz  16987  prmolefac  17008  prmgaplem7  17019  cshwshashlem1  17057  ressval3d  17207  firest  17386  xpsfeq  17518  funcres2c  17861  ex-chn2  18595  smndex1basss  18867  smndex1mgm  18869  smndex1mndlem  18871  mulgnn0gsum  19047  symgfix2  19382  pmtrprfval  19453  m1expaddsub  19464  psgnprfval  19487  gsumpr  19921  gsumzunsnd  19922  0ringnnzr  20497  frgpcyg  21548  cnmsgnsubg  21552  psgninv  21557  zrhpsgnelbas  21569  m2detleiblem1  22607  symgmatr01lem  22636  indiscld  23074  pnfnei  23203  mnfnei  23204  alexsubALTlem2  24031  alexsubALTlem3  24032  dscmet  24555  xrtgioo  24790  ishl2  25355  iunmbl2  25542  icombl  25549  ioombl  25550  recnprss  25889  recnperf  25890  dvexp2  25939  dvexp3  25963  dvne0f1  25997  plypf1  26195  taylfvallem1  26340  taylfval  26342  tayl0  26345  coseq0negpitopi  26485  logfac  26583  cxpexp  26650  pythag  26799  reasinsin  26878  harmonicbnd3  26989  lgslem4  27281  gausslemma2dlem0i  27345  lgsquadlem2  27362  2lgslem3  27385  2lgs  27388  2lgsoddprmlem3  27395  2sqnn0  27419  2sqnn  27420  ltsres  27644  nolesgn2o  27653  nogesgn1o  27655  nosep1o  27663  nosep2o  27664  noetalem2  27724  sltsun1  27798  sltsun2  27799  eln0s  28371  n0zs  28399  bdaypw2n0bndlem  28473  bdaypw2n0bnd  28474  lfgrnloop  29212  uhgr2edg  29295  usgredg4  29304  usgredg2v  29314  usgrexmplef  29346  nb3grprlem1  29467  uvtx01vtx  29484  wlk1walk  29725  upgriswlk  29727  pthdadjvtx  29814  upgrwlkdvdelem  29822  pthdlem2lem  29853  pthspthcyc  29889  2pthon3v  30029  clwwlkn  30114  clwwlkneq0  30117  eupth2lem3lem4  30319  konigsberg  30345  3vfriswmgrlem  30365  1to2vfriswmgr  30367  1to3vfriswmgr  30368  frgrregorufr0  30412  numclwlk1  30459  ex-pr  30518  shunssi  31457  cvmdi  32413  1neg1t1neg1  32830  iundisj2cnt  32891  fz1nnct  32893  xrge0iifiso  34119  esumpr2  34251  measiuns  34401  sxbrsigalem0  34455  bnj964  35125  subfacval3  35417  kur14lem7  35440  satfrnmapom  35598  gonar  35623  goalr  35625  mrsubcv  35738  nepss  35946  nnuni  35955  fz0n  35959  bccolsum  35967  dfon2lem7  36015  altopthsn  36189  elhf2  36403  nn0prpw  36551  dissym1  36649  ordcmp  36675  ttciunun  36739  bj-currypeirce  36867  bj-jaoi1  36882  bj-jaoi2  36883  bj-ififc  36893  bj-andnotim  36899  bj-nfimexal  36949  bj-sbsb  37190  bj-elsn12g  37413  bj-ideqg1  37524  finxpreclem2  37752  wl-equsal1i  37915  tan2h  37979  poimirlem23  38010  poimirlem32  38019  itg2addnclem  38038  orfa1  38452  orfa2  38453  inex3  38705  inxpex  38706  mopickr  38738  disjlem14  39268  elpadd0  40301  aks6d1c2p2  42604  sbor2  42697  sn-0ne2  42883  sn-0lt1  42965  hbtlem5  43573  omabs2  43777  safesnsupfiss  43859  safesnsupfidom1o  43861  safesnsupfilb  43862  rp-fakeimass  43956  rp-isfinite6  43962  pr2cv  43992  iunrelexp0  44146  relexpss1d  44149  relexpmulg  44154  iunrelexpmin2  44156  relexp01min  44157  relexp0a  44160  relexpxpmin  44161  relexpaddss  44162  clsk1indlem3  44487  ssrecnpr  44752  seff  44753  sblpnf  44754  expgrowthi  44777  dvconstbi  44778  19.33-2  44826  ax6e2ndeq  45003  en3lpVD  45288  undif3VD  45325  ax6e2ndeqVD  45352  ax6e2ndeqALT  45374  iooinlbub  45946  elprneb  47492  euoreqb  47572  2reu3  47573  afvpcfv0  47609  afvfv0bi  47615  afvco2  47639  afv2orxorb  47691  afv2ndeffv0  47723  afv2fv0b  47729  fvmptrabdm  47756  nnmul2  47793  2ltceilhalf  47795  ceilhalfnn  47803  minusmodnep2tmod  47822  iccpartltu  47900  iccpartgtl  47901  iccpartgt  47902  iccpartleu  47903  iccpartgel  47904  iccpartnel  47913  elsprel  47950  prsprel  47962  sprsymrelfolem2  47968  paireqne  47986  odz2prm2pw  48041  fmtnofac1  48048  fmtno4prmfac  48050  31prm  48075  lighneallem2  48084  lighneallem3  48085  lighneallem4b  48087  lighneallem4  48088  ppivalnnnprm  48106  ppivalnn  48110  zeo2ALTV  48162  nn0o1gt2ALTV  48185  nn0oALTV  48187  stgoldbwt  48267  sbgoldbwt  48268  sbgoldbalt  48272  sbgoldbm  48275  sbgoldbo  48278  nnsum3primesle9  48285  nnsum4primeseven  48291  nnsum4primesevenALTV  48292  wtgoldbnnsum4prm  48293  bgoldbnnsum3prm  48295  bgoldbtbndlem1  48296  bgoldbtbnd  48300  tgoldbach  48308  vopnbgrelself  48346  clnbgrgrim  48425  grtriproplem  48430  grtrif1o  48433  grtriclwlk3  48436  gpgedgvtx0  48552  gpgcubic  48570  gpg5nbgr3star  48572  gpgprismgr4cycllem3  48588  gpgprismgr4cycllem7  48592  gpgprismgr4cycllem10  48595  pgnbgreunbgrlem3  48609  pgnbgreunbgrlem6  48615  pgnbgreunbgr  48616  upgrwlkupwlk  48631  ztprmneprm  48838  islinindfis  48940  lindslinindsimp2lem5  48953  lindslinindsimp2  48954  lindsrng01  48959  elfzolborelfzop1  49010  flnn0div2ge  49024  blennn0elnn  49068  blen1b  49079  nnolog2flm1  49081  blengt1fldiv2p1  49084  0dig2pr01  49101  dignn0flhalf  49109  nn0sumshdiglemB  49111  nn0sumshdiglem1  49112  resum2sqorgt0  49200  rrx2xpref1o  49209  rrx2plord2  49213  itsclc0yqsol  49255  mosssn  49305  mo0sn  49306  mofsssn  49336  mofmo  49337  f1omo  49383  f1omoOLD  49384