Theorem jaoi 858

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

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

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 207  df-or 849

This theorem is referenced by:  jao1i  859  jaod  860  pm1.4  870  pm3.2ni  881  pm1.2  904  pm2.4  907  pm2.41  908  orim12i  909  pm1.5  920  pm2.42  945  jaoa  958  jaoian  959  pm4.44  999  andi  1010  ecase3  1033  cases2ALT  1049  consensus  1053  jaoi3  1061  1fpid3  1082  19.33  1886  19.33b  1887  nfim1  2207  dfsb2  2498  mooran1  2556  eueq3  3658  sbcor  3780  sspss  4043  sspsstr  4049  elun  4094  ssun  4136  inss  4189  raaan2  4463  ifbi  4490  ifcomnan  4524  rabsnifsb  4667  tpprceq3  4748  tppreqb  4749  pwpw0  4757  sssn  4770  snsssn  4785  preq12b  4794  prnebg  4800  preq12nebg  4807  elpr2elpr  4813  prproe  4849  3elpr2eq  4850  unissint  4915  zfpair  5359  axprg  5375  propeqop  5456  propssopi  5457  opthhausdorff  5466  opthhausdorff0  5467  iunopeqop  5470  relsnb  5752  iresn0n0  6014  sotri2  6087  sotri3  6088  somincom  6092  ordssun  6422  unizlim  6442  onxpdisj  6445  tpres  7150  sorpssuni  7680  ordeleqon  7730  ordunisuc  7777  orduninsuc  7788  tfinds  7805  limomss  7816  limom  7827  soxp  8073  ressuppssdif  8129  tfr2b  8329  omopthi  8591  domnsym  9035  ordfin  9144  brwdom  9476  cantnfvalf  9580  ttrclselem1  9640  djuss  9838  djuunxp  9839  eldju2ndl  9842  eldju2ndr  9843  djuun  9844  updjud  9852  iscard3  10009  cflim2  10179  sornom  10193  isfin5  10215  isfin6  10216  sdom2en01  10218  fin23lem29  10257  fin23lem30  10258  fin56  10309  fin67  10311  hsmexlem9  10341  axcc4dom  10357  axdc3lem2  10367  axdc3lem4  10369  brdom3  10444  winainflem  10610  r1tskina  10699  indpi  10824  ltxrlt  11210  nn0sub  12481  nn0n0n1ge2b  12500  nn0ge2m1nn  12501  xnn0xr  12509  xnn0nemnf  12515  elnn0z  12531  nn0lt10b  12585  nn0le2is012  12587  nn0ind-raph  12623  uzin  12818  indstr2  12871  nn0ledivnn  13051  xrnemnf  13062  xrnepnf  13063  mnfltxr  13072  xnn0n0n1ge2b  13077  xnn0ge0  13079  xnn0xaddcl  13181  xnn0lenn0nn0  13191  xnn0xadd0  13193  xmullem2  13211  rexmul  13217  xnn0xrge0  13453  elfzonlteqm1  13690  elfznelfzo  13722  injresinjlem  13739  injresinj  13740  fldiv4p1lem1div2  13788  fldiv4lem1div2  13790  modfzo0difsn  13899  ssnn0fi  13941  fsuppmapnn0fiubex  13948  m1expcl2  14041  m1expeven  14065  zzlesq  14162  sq01  14181  expnngt1  14197  nn0opthi  14226  facp1  14234  faclbnd3  14248  faclbnd4lem1  14249  faclbnd4lem3  14251  bcn1  14269  hashnemnf  14300  hashv01gt1  14301  hashneq0  14320  hashrabrsn  14328  hashrabsn01  14329  hashrabsn1  14330  hashunx  14342  hashsnle1  14373  hashfzp1  14387  hash2pwpr  14432  hashge2el2difr  14437  swrdnd2  14612  pfxnd0  14645  repswswrd  14740  relexpsucl  14987  relexpsucr  14988  relexpcnv  14991  relexprelg  14994  relexpdmg  14998  relexprng  15002  relexpfld  15005  relexpaddg  15009  sumz  15678  arisum  15819  arisum2  15820  pwdif  15827  ntrivcvg  15856  prod1  15903  fprodfac  15932  mod2eq1n2dvds  16310  mulsucdiv2z  16316  nn0o1gt2  16344  nno  16345  nn0o  16346  sumeven  16350  sumodd  16351  divalglem1  16357  divalglem6  16361  gcdaddmlem  16487  dfgcd2  16509  mulgcd  16511  lcmf  16596  lcmfunsnlem2lem2  16602  lcmfunsnlem2  16603  prm2orodd  16654  dfphi2  16738  nnnn0modprm0  16771  prm23lt5  16779  oddprmdvds  16868  4sqlem19  16928  ramz  16990  prmolefac  17011  prmgaplem7  17022  cshwshashlem1  17060  ressval3d  17210  firest  17389  xpsfeq  17521  funcres2c  17864  ex-chn2  18598  smndex1basss  18870  smndex1mgm  18872  smndex1mndlem  18874  mulgnn0gsum  19050  symgfix2  19385  pmtrprfval  19456  m1expaddsub  19467  psgnprfval  19490  gsumpr  19924  gsumzunsnd  19925  0ringnnzr  20496  frgpcyg  21566  cnmsgnsubg  21570  psgninv  21575  zrhpsgnelbas  21587  m2detleiblem1  22602  symgmatr01lem  22631  indiscld  23069  pnfnei  23198  mnfnei  23199  alexsubALTlem2  24026  alexsubALTlem3  24027  dscmet  24550  xrtgioo  24785  ishl2  25350  iunmbl2  25537  icombl  25544  ioombl  25545  recnprss  25884  recnperf  25885  dvexp2  25934  dvexp3  25958  dvne0f1  25992  plypf1  26190  taylfvallem1  26336  taylfval  26338  tayl0  26341  coseq0negpitopi  26483  logfac  26581  cxpexp  26648  pythag  26797  reasinsin  26876  harmonicbnd3  26988  lgslem4  27280  gausslemma2dlem0i  27344  lgsquadlem2  27361  2lgslem3  27384  2lgs  27387  2lgsoddprmlem3  27394  2sqnn0  27418  2sqnn  27419  ltsres  27643  nolesgn2o  27652  nogesgn1o  27654  nosep1o  27662  nosep2o  27663  noetalem2  27723  sltsun1  27797  sltsun2  27798  eln0s  28370  n0zs  28398  bdaypw2n0bndlem  28472  bdaypw2n0bnd  28473  lfgrnloop  29211  uhgr2edg  29294  usgredg4  29303  usgredg2v  29313  usgrexmplef  29345  nb3grprlem1  29466  uvtx01vtx  29483  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  32829  iundisj2cnt  32890  fz1nnct  32892  xrge0iifiso  34098  esumpr2  34230  measiuns  34380  sxbrsigalem0  34434  bnj964  35104  subfacval3  35390  kur14lem7  35413  satfrnmapom  35571  gonar  35596  goalr  35598  mrsubcv  35711  nepss  35919  nnuni  35928  fz0n  35932  bccolsum  35940  dfon2lem7  35988  altopthsn  36162  elhf2  36376  nn0prpw  36524  dissym1  36622  ordcmp  36648  ttciunun  36712  bj-currypeirce  36840  bj-jaoi1  36855  bj-jaoi2  36856  bj-ififc  36866  bj-andnotim  36872  bj-nfimexal  36922  bj-sbsb  37163  bj-elsn12g  37386  bj-ideqg1  37497  finxpreclem2  37723  wl-equsal1i  37886  tan2h  37950  poimirlem23  37981  poimirlem32  37990  itg2addnclem  38009  orfa1  38423  orfa2  38424  inex3  38676  inxpex  38677  mopickr  38709  disjlem14  39239  elpadd0  40272  aks6d1c2p2  42575  sbor2  42668  sn-0ne2  42855  sn-0lt1  42937  hbtlem5  43577  omabs2  43781  safesnsupfiss  43863  safesnsupfidom1o  43865  safesnsupfilb  43866  rp-fakeimass  43960  rp-isfinite6  43966  pr2cv  43996  iunrelexp0  44150  relexpss1d  44153  relexpmulg  44158  iunrelexpmin2  44160  relexp01min  44161  relexp0a  44164  relexpxpmin  44165  relexpaddss  44166  clsk1indlem3  44491  ssrecnpr  44756  seff  44757  sblpnf  44758  expgrowthi  44781  dvconstbi  44782  19.33-2  44830  ax6e2ndeq  45007  en3lpVD  45292  undif3VD  45329  ax6e2ndeqVD  45356  ax6e2ndeqALT  45378  iooinlbub  45952  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