Theorem jaoi 854

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

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

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 210  df-or 845

This theorem is referenced by:  jao1i  855  jaod  856  pm1.4  866  pm3.2ni  878  pm1.2  901  pm2.4  904  pm2.41  905  orim12i  906  pm1.5  917  pm2.42  940  jaoa  953  jaoian  954  pm4.44  994  andi  1005  ecase3  1028  cases2ALT  1044  consensus  1048  jaoi3  1056  1fpid3  1079  19.33  1885  19.33b  1886  nfim1  2197  dfsb2  2511  dfsb2ALT  2567  mooran1  2614  eueq3  3650  sbcor  3769  sspss  4027  sspsstr  4033  elun  4076  ssun  4116  inss  4165  raaan2  4422  ifbi  4446  ifcomnan  4479  elpr2OLD  4551  rabsnifsb  4618  tpprceq3  4697  tppreqb  4698  pwpw0  4706  sssn  4719  snsssn  4732  preq12b  4741  prnebg  4746  preq12nebg  4753  elpr2elpr  4759  pwsnOLD  4793  prproe  4798  3elpr2eq  4799  unissint  4862  zfpair  5287  propeqop  5362  propssopi  5363  opthhausdorff  5372  opthhausdorff0  5373  iunopeqop  5376  relsnb  5639  iresn0n0  5890  sotri2  5956  sotri3  5957  somincom  5961  ordssun  6258  onun2i  6274  unizlim  6275  onxpdisj  6278  tpres  6940  sorpssuni  7438  ordeleqon  7483  ordunisuc  7527  orduninsuc  7538  tfinds  7554  limomss  7565  limom  7575  soxp  7806  ressuppssdif  7834  tfr2b  8015  omopthi  8267  domnsym  8627  brwdom  9015  cantnfvalf  9112  djuss  9333  djuunxp  9334  eldju2ndl  9337  eldju2ndr  9338  djuun  9339  updjud  9347  iscard3  9504  cflim2  9674  sornom  9688  isfin5  9710  isfin6  9711  sdom2en01  9713  fin23lem29  9752  fin23lem30  9753  fin56  9804  fin67  9806  hsmexlem9  9836  axcc4dom  9852  axdc3lem2  9862  axdc3lem4  9864  brdom3  9939  winainflem  10104  r1tskina  10193  indpi  10318  ltxrlt  10700  nn0sub  11935  nn0n0n1ge2b  11951  nn0ge2m1nn  11952  xnn0xr  11960  xnn0nemnf  11966  elnn0z  11982  nn0lt10b  12032  nn0le2is012  12034  nn0ind-raph  12070  uzin  12266  indstr2  12315  nn0ledivnn  12490  xrnemnf  12500  xrnepnf  12501  mnfltxr  12510  xnn0n0n1ge2b  12514  xnn0ge0  12516  xnn0xaddcl  12616  xnn0lenn0nn0  12626  xnn0xadd0  12628  xmullem2  12646  rexmul  12652  xnn0xrge0  12884  elfzonlteqm1  13108  elfznelfzo  13137  injresinjlem  13152  injresinj  13153  fldiv4p1lem1div2  13200  fldiv4lem1div2  13202  modfzo0difsn  13306  ssnn0fi  13348  fsuppmapnn0fiubex  13355  m1expcl2  13447  m1expeven  13472  sq01  13582  expnngt1  13598  nn0opthi  13626  facp1  13634  faclbnd3  13648  faclbnd4lem1  13649  faclbnd4lem3  13651  bcn1  13669  hashnemnf  13700  hashv01gt1  13701  hashneq0  13721  hashrabrsn  13729  hashrabsn01  13730  hashrabsn1  13731  hashunx  13743  hashsnle1  13774  hashfzp1  13788  hash2pwpr  13830  hashge2el2difr  13835  swrdnd2  14008  pfxnd0  14041  repswswrd  14137  relexpsucl  14382  relexpsucr  14383  relexpcnv  14386  relexprelg  14389  relexpdmg  14393  relexprng  14397  relexpfld  14400  relexpaddg  14404  sumz  15071  arisum  15207  arisum2  15208  pwdif  15215  ntrivcvg  15245  prod1  15290  fprodfac  15319  mod2eq1n2dvds  15688  mulsucdiv2z  15694  nn0o1gt2  15722  nno  15723  nn0o  15724  sumeven  15728  sumodd  15729  divalglem1  15735  divalglem6  15739  gcdaddmlem  15862  dfgcd2  15884  mulgcd  15886  lcmf  15967  lcmfunsnlem2lem2  15973  lcmfunsnlem2  15974  prm2orodd  16025  dfphi2  16101  nnnn0modprm0  16133  prm23lt5  16141  oddprmdvds  16229  4sqlem19  16289  ramz  16351  prmolefac  16372  prmgaplem7  16383  cshwshashlem1  16421  ressval3d  16553  firest  16698  xpsfeq  16828  funcres2c  17163  smndex1basss  18062  smndex1mgm  18064  smndex1mndlem  18066  mulgnn0gsum  18226  symgfix2  18536  pmtrprfval  18607  m1expaddsub  18618  psgnprfval  18641  gsumpr  19068  gsumzunsnd  19069  sralem  19942  0ringnnzr  20035  frgpcyg  20265  cnmsgnsubg  20266  psgninv  20271  zrhpsgnelbas  20283  m2detleiblem1  21229  symgmatr01lem  21258  indiscld  21696  pnfnei  21825  mnfnei  21826  alexsubALTlem2  22653  alexsubALTlem3  22654  dscmet  23179  xrtgioo  23411  ishl2  23974  iunmbl2  24161  icombl  24168  ioombl  24169  recnprss  24507  recnperf  24508  dvexp2  24557  dvexp3  24581  dvne0f1  24615  plypf1  24809  taylfvallem1  24952  taylfval  24954  tayl0  24957  coseq0negpitopi  25096  logfac  25192  cxpexp  25259  pythag  25403  reasinsin  25482  harmonicbnd3  25593  lgslem4  25884  gausslemma2dlem0i  25948  lgsquadlem2  25965  2lgslem3  25988  2lgs  25991  2lgsoddprmlem3  25998  2sqnn0  26022  2sqnn  26023  cchhllem  26681  lfgrnloop  26918  uhgr2edg  26998  usgredg4  27007  usgredg2v  27017  usgrexmplef  27049  nb3grprlem1  27170  uvtx01vtx  27187  wlk1walk  27428  upgriswlk  27430  pthdadjvtx  27519  upgrwlkdvdelem  27525  pthdlem2lem  27556  2pthon3v  27729  clwwlkn  27811  clwwlkneq0  27814  eupth2lem3lem4  28016  konigsberg  28042  3vfriswmgrlem  28062  1to2vfriswmgr  28064  1to3vfriswmgr  28065  frgrregorufr0  28109  numclwlk1  28156  ex-pr  28215  shunssi  29151  cvmdi  30107  1neg1t1neg1  30499  iundisj2cnt  30548  fz1nnct  30552  xrge0iifiso  31288  esumpr2  31436  measiuns  31586  sxbrsigalem0  31639  bnj964  32325  subfacval3  32549  kur14lem7  32572  satfrnmapom  32730  gonar  32755  goalr  32757  mrsubcv  32870  nepss  33061  fz0n  33075  bccolsum  33084  dfon2lem7  33147  trpredlem1  33179  trpred0  33188  sltres  33282  nolesgn2o  33291  nosep1o  33299  altopthsn  33535  elhf2  33749  nn0prpw  33784  dissym1  33882  ordcmp  33908  bj-currypeirce  34005  bj-jaoi1  34017  bj-jaoi2  34018  bj-ififc  34028  bj-andnotim  34035  bj-nfimexal  34072  bj-sbsb  34275  bj-elsn12g  34477  bj-ideqg1  34579  finxpreclem2  34807  wl-equsal1i  34948  tan2h  35049  poimirlem23  35080  poimirlem32  35089  itg2addnclem  35108  orfa1  35523  orfa2  35524  imaexALTV  35747  inex3  35755  inxpex  35756  elpadd0  37105  sbor2  39395  sn-0ne2  39544  sn-0lt1  39587  hbtlem5  40072  rp-fakeimass  40220  rp-isfinite6  40226  pr2cv  40247  iunrelexp0  40403  relexpss1d  40406  relexpmulg  40411  iunrelexpmin2  40413  relexp01min  40414  relexp0a  40417  relexpxpmin  40418  relexpaddss  40419  clsk1indlem3  40746  ssrecnpr  41012  seff  41013  sblpnf  41014  expgrowthi  41037  dvconstbi  41038  19.33-2  41086  ax6e2ndeq  41265  en3lpVD  41551  undif3VD  41588  ax6e2ndeqVD  41615  ax6e2ndeqALT  41637  iooinlbub  42138  elprneb  43621  euoreqb  43665  2reu3  43666  afvpcfv0  43702  afvfv0bi  43708  afvco2  43732  afv2orxorb  43784  afv2ndeffv0  43816  afv2fv0b  43822  fvmptrabdm  43849  iccpartltu  43942  iccpartgtl  43943  iccpartgt  43944  iccpartleu  43945  iccpartgel  43946  iccpartnel  43955  elsprel  43992  prsprel  44004  sprsymrelfolem2  44010  paireqne  44028  odz2prm2pw  44080  fmtnofac1  44087  fmtno4prmfac  44089  31prm  44114  lighneallem2  44124  lighneallem3  44125  lighneallem4b  44127  lighneallem4  44128  zeo2ALTV  44189  nn0o1gt2ALTV  44212  nn0oALTV  44214  stgoldbwt  44294  sbgoldbwt  44295  sbgoldbalt  44299  sbgoldbm  44302  sbgoldbo  44305  nnsum3primesle9  44312  nnsum4primeseven  44318  nnsum4primesevenALTV  44319  wtgoldbnnsum4prm  44320  bgoldbnnsum3prm  44322  bgoldbtbndlem1  44323  bgoldbtbnd  44327  tgoldbach  44335  isomuspgrlem1  44345  upgrwlkupwlk  44368  ztprmneprm  44749  islinindfis  44858  lindslinindsimp2lem5  44871  lindslinindsimp2  44872  lindsrng01  44877  elfzolborelfzop1  44928  flnn0div2ge  44947  blennn0elnn  44991  blen1b  45002  nnolog2flm1  45004  blengt1fldiv2p1  45007  0dig2pr01  45024  dignn0flhalf  45032  nn0sumshdiglemB  45034  nn0sumshdiglem1  45035  resum2sqorgt0  45123  rrx2xpref1o  45132  rrx2plord2  45136  itsclc0yqsol  45178