Theorem jaoi 857

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 851	. . 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 847

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 848

This theorem is referenced by:  jao1i  858  jaod  859  pm1.4  869  pm3.2ni  880  pm1.2  903  pm2.4  906  pm2.41  907  orim12i  908  pm1.5  919  pm2.42  944  jaoa  957  jaoian  958  pm4.44  998  andi  1009  ecase3  1032  cases2ALT  1048  consensus  1052  jaoi3  1060  1fpid3  1081  19.33  1884  19.33b  1885  nfim1  2200  dfsb2  2491  mooran1  2548  eueq3  3679  sbcor  3801  sspss  4061  sspsstr  4067  elun  4112  ssun  4154  inss  4207  raaan2  4480  ifbi  4507  ifcomnan  4541  rabsnifsb  4682  tpprceq3  4764  tppreqb  4765  pwpw0  4773  sssn  4786  snsssn  4801  preq12b  4810  prnebg  4816  preq12nebg  4823  elpr2elpr  4829  prproe  4865  3elpr2eq  4866  unissint  4932  zfpair  5371  propeqop  5462  propssopi  5463  opthhausdorff  5472  opthhausdorff0  5473  iunopeqop  5476  relsnb  5756  iresn0n0  6014  sotri2  6090  sotri3  6091  somincom  6095  ordssun  6424  unizlim  6445  onxpdisj  6448  tpres  7157  sorpssuni  7688  ordeleqon  7738  ordunisuc  7787  orduninsuc  7799  tfinds  7816  limomss  7827  limom  7838  soxp  8085  ressuppssdif  8141  tfr2b  8341  omopthi  8602  domnsym  9044  brwdom  9496  cantnfvalf  9594  ttrclselem1  9654  djuss  9849  djuunxp  9850  eldju2ndl  9853  eldju2ndr  9854  djuun  9855  updjud  9863  iscard3  10022  cflim2  10192  sornom  10206  isfin5  10228  isfin6  10229  sdom2en01  10231  fin23lem29  10270  fin23lem30  10271  fin56  10322  fin67  10324  hsmexlem9  10354  axcc4dom  10370  axdc3lem2  10380  axdc3lem4  10382  brdom3  10457  winainflem  10622  r1tskina  10711  indpi  10836  ltxrlt  11220  nn0sub  12468  nn0n0n1ge2b  12487  nn0ge2m1nn  12488  xnn0xr  12496  xnn0nemnf  12502  elnn0z  12518  nn0lt10b  12572  nn0le2is012  12574  nn0ind-raph  12610  uzin  12809  indstr2  12862  nn0ledivnn  13042  xrnemnf  13053  xrnepnf  13054  mnfltxr  13063  xnn0n0n1ge2b  13068  xnn0ge0  13070  xnn0xaddcl  13171  xnn0lenn0nn0  13181  xnn0xadd0  13183  xmullem2  13201  rexmul  13207  xnn0xrge0  13443  elfzonlteqm1  13678  elfznelfzo  13709  injresinjlem  13724  injresinj  13725  fldiv4p1lem1div2  13773  fldiv4lem1div2  13775  modfzo0difsn  13884  ssnn0fi  13926  fsuppmapnn0fiubex  13933  m1expcl2  14026  m1expeven  14050  zzlesq  14147  sq01  14166  expnngt1  14182  nn0opthi  14211  facp1  14219  faclbnd3  14233  faclbnd4lem1  14234  faclbnd4lem3  14236  bcn1  14254  hashnemnf  14285  hashv01gt1  14286  hashneq0  14305  hashrabrsn  14313  hashrabsn01  14314  hashrabsn1  14315  hashunx  14327  hashsnle1  14358  hashfzp1  14372  hash2pwpr  14417  hashge2el2difr  14422  swrdnd2  14596  pfxnd0  14629  repswswrd  14725  relexpsucl  14973  relexpsucr  14974  relexpcnv  14977  relexprelg  14980  relexpdmg  14984  relexprng  14988  relexpfld  14991  relexpaddg  14995  sumz  15664  arisum  15802  arisum2  15803  pwdif  15810  ntrivcvg  15839  prod1  15886  fprodfac  15915  mod2eq1n2dvds  16293  mulsucdiv2z  16299  nn0o1gt2  16327  nno  16328  nn0o  16329  sumeven  16333  sumodd  16334  divalglem1  16340  divalglem6  16344  gcdaddmlem  16470  dfgcd2  16492  mulgcd  16494  lcmf  16579  lcmfunsnlem2lem2  16585  lcmfunsnlem2  16586  prm2orodd  16637  dfphi2  16720  nnnn0modprm0  16753  prm23lt5  16761  oddprmdvds  16850  4sqlem19  16910  ramz  16972  prmolefac  16993  prmgaplem7  17004  cshwshashlem1  17042  ressval3d  17192  firest  17371  xpsfeq  17502  funcres2c  17841  smndex1basss  18808  smndex1mgm  18810  smndex1mndlem  18812  mulgnn0gsum  18988  symgfix2  19322  pmtrprfval  19393  m1expaddsub  19404  psgnprfval  19427  gsumpr  19861  gsumzunsnd  19862  0ringnnzr  20410  frgpcyg  21459  cnmsgnsubg  21462  psgninv  21467  zrhpsgnelbas  21479  m2detleiblem1  22487  symgmatr01lem  22516  indiscld  22954  pnfnei  23083  mnfnei  23084  alexsubALTlem2  23911  alexsubALTlem3  23912  dscmet  24436  xrtgioo  24671  ishl2  25246  iunmbl2  25434  icombl  25441  ioombl  25442  recnprss  25781  recnperf  25782  dvexp2  25834  dvexp3  25858  dvne0f1  25893  plypf1  26093  taylfvallem1  26240  taylfval  26242  tayl0  26245  coseq0negpitopi  26388  logfac  26486  cxpexp  26553  pythag  26703  reasinsin  26782  harmonicbnd3  26894  lgslem4  27187  gausslemma2dlem0i  27251  lgsquadlem2  27268  2lgslem3  27291  2lgs  27294  2lgsoddprmlem3  27301  2sqnn0  27325  2sqnn  27326  sltres  27550  nolesgn2o  27559  nogesgn1o  27561  nosep1o  27569  nosep2o  27570  noetalem2  27630  ssltun1  27696  ssltun2  27697  eln0s  28227  n0zs  28253  lfgrnloop  29028  uhgr2edg  29111  usgredg4  29120  usgredg2v  29130  usgrexmplef  29162  nb3grprlem1  29283  uvtx01vtx  29300  wlk1walk  29542  upgriswlk  29544  pthdadjvtx  29631  upgrwlkdvdelem  29639  pthdlem2lem  29670  pthspthcyc  29706  2pthon3v  29846  clwwlkn  29928  clwwlkneq0  29931  eupth2lem3lem4  30133  konigsberg  30159  3vfriswmgrlem  30179  1to2vfriswmgr  30181  1to3vfriswmgr  30182  frgrregorufr0  30226  numclwlk1  30273  ex-pr  30332  shunssi  31270  cvmdi  32226  1neg1t1neg1  32634  iundisj2cnt  32695  fz1nnct  32699  xrge0iifiso  33898  esumpr2  34030  measiuns  34180  sxbrsigalem0  34235  bnj964  34906  subfacval3  35149  kur14lem7  35172  satfrnmapom  35330  gonar  35355  goalr  35357  mrsubcv  35470  nepss  35678  nnuni  35687  fz0n  35691  bccolsum  35699  dfon2lem7  35750  altopthsn  35922  elhf2  36136  nn0prpw  36284  dissym1  36382  ordcmp  36408  bj-currypeirce  36518  bj-jaoi1  36532  bj-jaoi2  36533  bj-ififc  36543  bj-andnotim  36549  bj-nfimexal  36587  bj-sbsb  36798  bj-elsn12g  37021  bj-ideqg1  37125  finxpreclem2  37351  wl-equsal1i  37505  tan2h  37579  poimirlem23  37610  poimirlem32  37619  itg2addnclem  37638  orfa1  38052  orfa2  38053  inex3  38293  inxpex  38294  mopickr  38318  disjlem14  38763  elpadd0  39776  aks6d1c2p2  42080  sbor2  42173  sn-0ne2  42367  sn-0lt1  42436  hbtlem5  43090  omabs2  43294  safesnsupfiss  43377  safesnsupfidom1o  43379  safesnsupfilb  43380  rp-fakeimass  43474  rp-isfinite6  43480  pr2cv  43510  iunrelexp0  43664  relexpss1d  43667  relexpmulg  43672  iunrelexpmin2  43674  relexp01min  43675  relexp0a  43678  relexpxpmin  43679  relexpaddss  43680  clsk1indlem3  44005  ssrecnpr  44270  seff  44271  sblpnf  44272  expgrowthi  44295  dvconstbi  44296  19.33-2  44344  ax6e2ndeq  44522  en3lpVD  44807  undif3VD  44844  ax6e2ndeqVD  44871  ax6e2ndeqALT  44893  iooinlbub  45472  elprneb  47003  euoreqb  47083  2reu3  47084  afvpcfv0  47120  afvfv0bi  47126  afvco2  47150  afv2orxorb  47202  afv2ndeffv0  47234  afv2fv0b  47240  fvmptrabdm  47267  2ltceilhalf  47302  ceilhalfnn  47310  minusmodnep2tmod  47327  iccpartltu  47399  iccpartgtl  47400  iccpartgt  47401  iccpartleu  47402  iccpartgel  47403  iccpartnel  47412  elsprel  47449  prsprel  47461  sprsymrelfolem2  47467  paireqne  47485  odz2prm2pw  47537  fmtnofac1  47544  fmtno4prmfac  47546  31prm  47571  lighneallem2  47580  lighneallem3  47581  lighneallem4b  47583  lighneallem4  47584  zeo2ALTV  47645  nn0o1gt2ALTV  47668  nn0oALTV  47670  stgoldbwt  47750  sbgoldbwt  47751  sbgoldbalt  47755  sbgoldbm  47758  sbgoldbo  47761  nnsum3primesle9  47768  nnsum4primeseven  47774  nnsum4primesevenALTV  47775  wtgoldbnnsum4prm  47776  bgoldbnnsum3prm  47778  bgoldbtbndlem1  47779  bgoldbtbnd  47783  tgoldbach  47791  vopnbgrelself  47828  clnbgrgrim  47907  grtriproplem  47911  grtrif1o  47914  grtriclwlk3  47917  gpgedgvtx0  48025  gpgcubic  48043  gpg5nbgr3star  48045  gpgprismgr4cycllem3  48060  gpgprismgr4cycllem7  48064  gpgprismgr4cycllem10  48067  pgnbgreunbgrlem3  48081  pgnbgreunbgrlem6  48087  pgnbgreunbgr  48088  upgrwlkupwlk  48101  ztprmneprm  48308  islinindfis  48411  lindslinindsimp2lem5  48424  lindslinindsimp2  48425  lindsrng01  48430  elfzolborelfzop1  48481  flnn0div2ge  48495  blennn0elnn  48539  blen1b  48550  nnolog2flm1  48552  blengt1fldiv2p1  48555  0dig2pr01  48572  dignn0flhalf  48580  nn0sumshdiglemB  48582  nn0sumshdiglem1  48583  resum2sqorgt0  48671  rrx2xpref1o  48680  rrx2plord2  48684  itsclc0yqsol  48726  mosssn  48776  mo0sn  48777  mofsssn  48807  mofmo  48808  f1omo  48854  f1omoOLD  48855