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  1881  19.33b  1882  nfim1  2196  dfsb2  2495  mooran1  2552  eueq3  3719  sbcor  3844  sspss  4111  sspsstr  4117  elun  4162  ssun  4204  inss  4254  raaan2  4526  ifbi  4552  ifcomnan  4586  rabsnifsb  4726  tpprceq3  4808  tppreqb  4809  pwpw0  4817  sssn  4830  snsssn  4845  preq12b  4854  prnebg  4860  preq12nebg  4867  elpr2elpr  4873  prproe  4909  3elpr2eq  4910  unissint  4976  zfpair  5426  propeqop  5516  propssopi  5517  opthhausdorff  5526  opthhausdorff0  5527  iunopeqop  5530  relsnb  5814  iresn0n0  6073  sotri2  6151  sotri3  6152  somincom  6156  ordssun  6487  unizlim  6508  onxpdisj  6511  tpres  7220  sorpssuni  7750  ordeleqon  7800  ordunisuc  7851  orduninsuc  7863  tfinds  7880  limomss  7891  limom  7902  soxp  8152  ressuppssdif  8208  tfr2b  8434  omopthi  8697  domnsym  9137  brwdom  9604  cantnfvalf  9702  ttrclselem1  9762  djuss  9957  djuunxp  9958  eldju2ndl  9961  eldju2ndr  9962  djuun  9963  updjud  9971  iscard3  10130  cflim2  10300  sornom  10314  isfin5  10336  isfin6  10337  sdom2en01  10339  fin23lem29  10378  fin23lem30  10379  fin56  10430  fin67  10432  hsmexlem9  10462  axcc4dom  10478  axdc3lem2  10488  axdc3lem4  10490  brdom3  10565  winainflem  10730  r1tskina  10819  indpi  10944  ltxrlt  11328  nn0sub  12573  nn0n0n1ge2b  12592  nn0ge2m1nn  12593  xnn0xr  12601  xnn0nemnf  12607  elnn0z  12623  nn0lt10b  12677  nn0le2is012  12679  nn0ind-raph  12715  uzin  12915  indstr2  12966  nn0ledivnn  13145  xrnemnf  13156  xrnepnf  13157  mnfltxr  13166  xnn0n0n1ge2b  13170  xnn0ge0  13172  xnn0xaddcl  13273  xnn0lenn0nn0  13283  xnn0xadd0  13285  xmullem2  13303  rexmul  13309  xnn0xrge0  13542  elfzonlteqm1  13776  elfznelfzo  13807  injresinjlem  13822  injresinj  13823  fldiv4p1lem1div2  13871  fldiv4lem1div2  13873  modfzo0difsn  13980  ssnn0fi  14022  fsuppmapnn0fiubex  14029  m1expcl2  14122  m1expeven  14146  zzlesq  14241  sq01  14260  expnngt1  14276  nn0opthi  14305  facp1  14313  faclbnd3  14327  faclbnd4lem1  14328  faclbnd4lem3  14330  bcn1  14348  hashnemnf  14379  hashv01gt1  14380  hashneq0  14399  hashrabrsn  14407  hashrabsn01  14408  hashrabsn1  14409  hashunx  14421  hashsnle1  14452  hashfzp1  14466  hash2pwpr  14511  hashge2el2difr  14516  swrdnd2  14689  pfxnd0  14722  repswswrd  14818  relexpsucl  15066  relexpsucr  15067  relexpcnv  15070  relexprelg  15073  relexpdmg  15077  relexprng  15081  relexpfld  15084  relexpaddg  15088  sumz  15754  arisum  15892  arisum2  15893  pwdif  15900  ntrivcvg  15929  prod1  15976  fprodfac  16005  mod2eq1n2dvds  16380  mulsucdiv2z  16386  nn0o1gt2  16414  nno  16415  nn0o  16416  sumeven  16420  sumodd  16421  divalglem1  16427  divalglem6  16431  gcdaddmlem  16557  dfgcd2  16579  mulgcd  16581  lcmf  16666  lcmfunsnlem2lem2  16672  lcmfunsnlem2  16673  prm2orodd  16724  dfphi2  16807  nnnn0modprm0  16839  prm23lt5  16847  oddprmdvds  16936  4sqlem19  16996  ramz  17058  prmolefac  17079  prmgaplem7  17090  cshwshashlem1  17129  ressval3d  17291  ressval3dOLD  17292  firest  17478  xpsfeq  17609  funcres2c  17954  smndex1basss  18930  smndex1mgm  18932  smndex1mndlem  18934  mulgnn0gsum  19110  symgfix2  19448  pmtrprfval  19519  m1expaddsub  19530  psgnprfval  19553  gsumpr  19987  gsumzunsnd  19988  0ringnnzr  20541  sralemOLD  21193  frgpcyg  21609  cnmsgnsubg  21612  psgninv  21617  zrhpsgnelbas  21629  m2detleiblem1  22645  symgmatr01lem  22674  indiscld  23114  pnfnei  23243  mnfnei  23244  alexsubALTlem2  24071  alexsubALTlem3  24072  dscmet  24600  xrtgioo  24841  ishl2  25417  iunmbl2  25605  icombl  25612  ioombl  25613  recnprss  25953  recnperf  25954  dvexp2  26006  dvexp3  26030  dvne0f1  26065  plypf1  26265  taylfvallem1  26412  taylfval  26414  tayl0  26417  coseq0negpitopi  26559  logfac  26657  cxpexp  26724  pythag  26874  reasinsin  26953  harmonicbnd3  27065  lgslem4  27358  gausslemma2dlem0i  27422  lgsquadlem2  27439  2lgslem3  27462  2lgs  27465  2lgsoddprmlem3  27472  2sqnn0  27496  2sqnn  27497  sltres  27721  nolesgn2o  27730  nogesgn1o  27732  nosep1o  27740  nosep2o  27741  noetalem2  27801  ssltun1  27867  ssltun2  27868  eln0s  28372  n0zs  28389  cchhllemOLD  28916  lfgrnloop  29156  uhgr2edg  29239  usgredg4  29248  usgredg2v  29258  usgrexmplef  29290  nb3grprlem1  29411  uvtx01vtx  29428  wlk1walk  29671  upgriswlk  29673  pthdadjvtx  29762  upgrwlkdvdelem  29768  pthdlem2lem  29799  2pthon3v  29972  clwwlkn  30054  clwwlkneq0  30057  eupth2lem3lem4  30259  konigsberg  30285  3vfriswmgrlem  30305  1to2vfriswmgr  30307  1to3vfriswmgr  30308  frgrregorufr0  30352  numclwlk1  30399  ex-pr  30458  shunssi  31396  cvmdi  32352  1neg1t1neg1  32754  iundisj2cnt  32806  fz1nnct  32810  xrge0iifiso  33895  esumpr2  34047  measiuns  34197  sxbrsigalem0  34252  bnj964  34935  subfacval3  35173  kur14lem7  35196  satfrnmapom  35354  gonar  35379  goalr  35381  mrsubcv  35494  nepss  35697  nnuni  35706  fz0n  35710  bccolsum  35718  dfon2lem7  35770  altopthsn  35942  elhf2  36156  nn0prpw  36305  dissym1  36403  ordcmp  36429  bj-currypeirce  36539  bj-jaoi1  36553  bj-jaoi2  36554  bj-ififc  36564  bj-andnotim  36570  bj-nfimexal  36608  bj-sbsb  36819  bj-elsn12g  37042  bj-ideqg1  37146  finxpreclem2  37372  wl-equsal1i  37524  tan2h  37598  poimirlem23  37629  poimirlem32  37638  itg2addnclem  37657  orfa1  38071  orfa2  38072  imaexALTV  38311  inex3  38319  inxpex  38320  mopickr  38344  disjlem14  38779  elpadd0  39791  aks6d1c2p2  42100  sbor2  42229  sn-0ne2  42412  sn-0lt1  42469  hbtlem5  43116  omabs2  43321  safesnsupfiss  43404  safesnsupfidom1o  43406  safesnsupfilb  43407  rp-fakeimass  43501  rp-isfinite6  43507  pr2cv  43537  iunrelexp0  43691  relexpss1d  43694  relexpmulg  43699  iunrelexpmin2  43701  relexp01min  43702  relexp0a  43705  relexpxpmin  43706  relexpaddss  43707  clsk1indlem3  44032  ssrecnpr  44303  seff  44304  sblpnf  44305  expgrowthi  44328  dvconstbi  44329  19.33-2  44377  ax6e2ndeq  44556  en3lpVD  44842  undif3VD  44879  ax6e2ndeqVD  44906  ax6e2ndeqALT  44928  iooinlbub  45453  elprneb  46978  euoreqb  47058  2reu3  47059  afvpcfv0  47095  afvfv0bi  47101  afvco2  47125  afv2orxorb  47177  afv2ndeffv0  47209  afv2fv0b  47215  fvmptrabdm  47242  minusmodnep2tmod  47292  iccpartltu  47349  iccpartgtl  47350  iccpartgt  47351  iccpartleu  47352  iccpartgel  47353  iccpartnel  47362  elsprel  47399  prsprel  47411  sprsymrelfolem2  47417  paireqne  47435  odz2prm2pw  47487  fmtnofac1  47494  fmtno4prmfac  47496  31prm  47521  lighneallem2  47530  lighneallem3  47531  lighneallem4b  47533  lighneallem4  47534  zeo2ALTV  47595  nn0o1gt2ALTV  47618  nn0oALTV  47620  stgoldbwt  47700  sbgoldbwt  47701  sbgoldbalt  47705  sbgoldbm  47708  sbgoldbo  47711  nnsum3primesle9  47718  nnsum4primeseven  47724  nnsum4primesevenALTV  47725  wtgoldbnnsum4prm  47726  bgoldbnnsum3prm  47728  bgoldbtbndlem1  47729  bgoldbtbnd  47733  tgoldbach  47741  vopnbgrelself  47778  clnbgrgrim  47839  grtriproplem  47843  grtrif1o  47846  grtriclwlk3  47849  2ltceilhalf  47949  gpgedgvtx0  47953  gpgcubic  47969  gpg5nbgr3star  47971  upgrwlkupwlk  47983  ztprmneprm  48191  islinindfis  48294  lindslinindsimp2lem5  48307  lindslinindsimp2  48308  lindsrng01  48313  elfzolborelfzop1  48364  flnn0div2ge  48382  blennn0elnn  48426  blen1b  48437  nnolog2flm1  48439  blengt1fldiv2p1  48442  0dig2pr01  48459  dignn0flhalf  48467  nn0sumshdiglemB  48469  nn0sumshdiglem1  48470  resum2sqorgt0  48558  rrx2xpref1o  48567  rrx2plord2  48571  itsclc0yqsol  48613  mosssn  48662  mo0sn  48663  mofsssn  48675  mofmo  48676  f1omo  48690