Theorem jaoi 855

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 849	. . 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 845

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 206  df-or 846

This theorem is referenced by:  jao1i  856  jaod  857  pm1.4  867  pm3.2ni  879  pm1.2  902  pm2.4  905  pm2.41  906  orim12i  907  pm1.5  918  pm2.42  941  jaoa  954  jaoian  955  pm4.44  995  andi  1006  ecase3  1030  cases2ALT  1047  consensus  1051  jaoi3  1059  1fpid3  1082  19.33  1887  19.33b  1888  nfim1  2192  dfsb2  2492  mooran1  2549  eueq3  3707  sbcor  3830  sspss  4099  sspsstr  4105  elun  4148  ssun  4189  inss  4238  raaan2  4524  ifbi  4550  ifcomnan  4584  elpr2OLD  4654  rabsnifsb  4726  tpprceq3  4807  tppreqb  4808  pwpw0  4816  sssn  4829  snsssn  4842  preq12b  4851  prnebg  4856  preq12nebg  4863  elpr2elpr  4869  pwsnOLD  4901  prproe  4906  3elpr2eq  4907  unissint  4976  zfpair  5419  propeqop  5507  propssopi  5508  opthhausdorff  5517  opthhausdorff0  5518  iunopeqop  5521  relsnb  5802  iresn0n0  6053  sotri2  6130  sotri3  6131  somincom  6135  ordssun  6466  unizlim  6487  onxpdisj  6490  tpres  7204  sorpssuni  7724  ordeleqon  7771  ordunisuc  7822  orduninsuc  7834  tfinds  7851  limomss  7862  limom  7873  soxp  8117  ressuppssdif  8172  tfr2b  8398  omopthi  8662  domnsym  9101  brwdom  9564  cantnfvalf  9662  ttrclselem1  9722  djuss  9917  djuunxp  9918  eldju2ndl  9921  eldju2ndr  9922  djuun  9923  updjud  9931  iscard3  10090  cflim2  10260  sornom  10274  isfin5  10296  isfin6  10297  sdom2en01  10299  fin23lem29  10338  fin23lem30  10339  fin56  10390  fin67  10392  hsmexlem9  10422  axcc4dom  10438  axdc3lem2  10448  axdc3lem4  10450  brdom3  10525  winainflem  10690  r1tskina  10779  indpi  10904  ltxrlt  11286  nn0sub  12524  nn0n0n1ge2b  12542  nn0ge2m1nn  12543  xnn0xr  12551  xnn0nemnf  12557  elnn0z  12573  nn0lt10b  12626  nn0le2is012  12628  nn0ind-raph  12664  uzin  12864  indstr2  12913  nn0ledivnn  13089  xrnemnf  13099  xrnepnf  13100  mnfltxr  13109  xnn0n0n1ge2b  13113  xnn0ge0  13115  xnn0xaddcl  13216  xnn0lenn0nn0  13226  xnn0xadd0  13228  xmullem2  13246  rexmul  13252  xnn0xrge0  13485  elfzonlteqm1  13710  elfznelfzo  13739  injresinjlem  13754  injresinj  13755  fldiv4p1lem1div2  13802  fldiv4lem1div2  13804  modfzo0difsn  13910  ssnn0fi  13952  fsuppmapnn0fiubex  13959  m1expcl2  14053  m1expeven  14077  zzlesq  14172  sq01  14190  expnngt1  14206  nn0opthi  14232  facp1  14240  faclbnd3  14254  faclbnd4lem1  14255  faclbnd4lem3  14257  bcn1  14275  hashnemnf  14306  hashv01gt1  14307  hashneq0  14326  hashrabrsn  14334  hashrabsn01  14335  hashrabsn1  14336  hashunx  14348  hashsnle1  14379  hashfzp1  14393  hash2pwpr  14439  hashge2el2difr  14444  swrdnd2  14607  pfxnd0  14640  repswswrd  14736  relexpsucl  14980  relexpsucr  14981  relexpcnv  14984  relexprelg  14987  relexpdmg  14991  relexprng  14995  relexpfld  14998  relexpaddg  15002  sumz  15670  arisum  15808  arisum2  15809  pwdif  15816  ntrivcvg  15845  prod1  15890  fprodfac  15919  mod2eq1n2dvds  16292  mulsucdiv2z  16298  nn0o1gt2  16326  nno  16327  nn0o  16328  sumeven  16332  sumodd  16333  divalglem1  16339  divalglem6  16343  gcdaddmlem  16467  dfgcd2  16490  mulgcd  16492  lcmf  16572  lcmfunsnlem2lem2  16578  lcmfunsnlem2  16579  prm2orodd  16630  dfphi2  16709  nnnn0modprm0  16741  prm23lt5  16749  oddprmdvds  16838  4sqlem19  16898  ramz  16960  prmolefac  16981  prmgaplem7  16992  cshwshashlem1  17031  ressval3d  17193  ressval3dOLD  17194  firest  17380  xpsfeq  17511  funcres2c  17854  smndex1basss  18788  smndex1mgm  18790  smndex1mndlem  18792  mulgnn0gsum  18962  symgfix2  19286  pmtrprfval  19357  m1expaddsub  19368  psgnprfval  19391  gsumpr  19825  gsumzunsnd  19826  0ringnnzr  20306  sralemOLD  20797  frgpcyg  21135  cnmsgnsubg  21136  psgninv  21141  zrhpsgnelbas  21153  m2detleiblem1  22133  symgmatr01lem  22162  indiscld  22602  pnfnei  22731  mnfnei  22732  alexsubALTlem2  23559  alexsubALTlem3  23560  dscmet  24088  xrtgioo  24329  ishl2  24894  iunmbl2  25081  icombl  25088  ioombl  25089  recnprss  25428  recnperf  25429  dvexp2  25478  dvexp3  25502  dvne0f1  25536  plypf1  25733  taylfvallem1  25876  taylfval  25878  tayl0  25881  coseq0negpitopi  26020  logfac  26116  cxpexp  26183  pythag  26329  reasinsin  26408  harmonicbnd3  26519  lgslem4  26810  gausslemma2dlem0i  26874  lgsquadlem2  26891  2lgslem3  26914  2lgs  26917  2lgsoddprmlem3  26924  2sqnn0  26948  2sqnn  26949  sltres  27172  nolesgn2o  27181  nogesgn1o  27183  nosep1o  27191  nosep2o  27192  noetalem2  27252  ssltun1  27317  ssltun2  27318  cchhllemOLD  28183  lfgrnloop  28423  uhgr2edg  28503  usgredg4  28512  usgredg2v  28522  usgrexmplef  28554  nb3grprlem1  28675  uvtx01vtx  28692  wlk1walk  28934  upgriswlk  28936  pthdadjvtx  29025  upgrwlkdvdelem  29031  pthdlem2lem  29062  2pthon3v  29235  clwwlkn  29317  clwwlkneq0  29320  eupth2lem3lem4  29522  konigsberg  29548  3vfriswmgrlem  29568  1to2vfriswmgr  29570  1to3vfriswmgr  29571  frgrregorufr0  29615  numclwlk1  29662  ex-pr  29721  shunssi  30659  cvmdi  31615  1neg1t1neg1  32000  iundisj2cnt  32048  fz1nnct  32052  xrge0iifiso  32984  esumpr2  33134  measiuns  33284  sxbrsigalem0  33339  bnj964  34023  subfacval3  34249  kur14lem7  34272  satfrnmapom  34430  gonar  34455  goalr  34457  mrsubcv  34570  nepss  34762  nnuni  34771  fz0n  34775  bccolsum  34784  dfon2lem7  34836  altopthsn  35008  elhf2  35222  nn0prpw  35300  dissym1  35398  ordcmp  35424  bj-currypeirce  35525  bj-jaoi1  35540  bj-jaoi2  35541  bj-ififc  35551  bj-andnotim  35558  bj-nfimexal  35595  bj-sbsb  35807  bj-elsn12g  36033  bj-ideqg1  36137  finxpreclem2  36363  wl-equsal1i  36504  tan2h  36572  poimirlem23  36603  poimirlem32  36612  itg2addnclem  36631  orfa1  37045  orfa2  37046  imaexALTV  37291  inex3  37299  inxpex  37300  mopickr  37324  disjlem14  37760  elpadd0  38772  aks6d1c2p2  41049  sbor2  41120  sn-0ne2  41367  sn-0lt1  41423  hbtlem5  41958  omabs2  42170  safesnsupfiss  42254  safesnsupfidom1o  42256  safesnsupfilb  42257  rp-fakeimass  42351  rp-isfinite6  42357  pr2cv  42387  iunrelexp0  42541  relexpss1d  42544  relexpmulg  42549  iunrelexpmin2  42551  relexp01min  42552  relexp0a  42555  relexpxpmin  42556  relexpaddss  42557  clsk1indlem3  42882  ssrecnpr  43155  seff  43156  sblpnf  43157  expgrowthi  43180  dvconstbi  43181  19.33-2  43229  ax6e2ndeq  43408  en3lpVD  43694  undif3VD  43731  ax6e2ndeqVD  43758  ax6e2ndeqALT  43780  iooinlbub  44299  elprneb  45824  euoreqb  45902  2reu3  45903  afvpcfv0  45939  afvfv0bi  45945  afvco2  45969  afv2orxorb  46021  afv2ndeffv0  46053  afv2fv0b  46059  fvmptrabdm  46086  iccpartltu  46178  iccpartgtl  46179  iccpartgt  46180  iccpartleu  46181  iccpartgel  46182  iccpartnel  46191  elsprel  46228  prsprel  46240  sprsymrelfolem2  46246  paireqne  46264  odz2prm2pw  46316  fmtnofac1  46323  fmtno4prmfac  46325  31prm  46350  lighneallem2  46359  lighneallem3  46360  lighneallem4b  46362  lighneallem4  46363  zeo2ALTV  46424  nn0o1gt2ALTV  46447  nn0oALTV  46449  stgoldbwt  46529  sbgoldbwt  46530  sbgoldbalt  46534  sbgoldbm  46537  sbgoldbo  46540  nnsum3primesle9  46547  nnsum4primeseven  46553  nnsum4primesevenALTV  46554  wtgoldbnnsum4prm  46555  bgoldbnnsum3prm  46557  bgoldbtbndlem1  46558  bgoldbtbnd  46562  tgoldbach  46570  isomuspgrlem1  46580  upgrwlkupwlk  46603  ztprmneprm  47108  islinindfis  47214  lindslinindsimp2lem5  47227  lindslinindsimp2  47228  lindsrng01  47233  elfzolborelfzop1  47284  flnn0div2ge  47303  blennn0elnn  47347  blen1b  47358  nnolog2flm1  47360  blengt1fldiv2p1  47363  0dig2pr01  47380  dignn0flhalf  47388  nn0sumshdiglemB  47390  nn0sumshdiglem1  47391  resum2sqorgt0  47479  rrx2xpref1o  47488  rrx2plord2  47492  itsclc0yqsol  47534  mosssn  47583  mo0sn  47584  mofsssn  47596  mofmo  47597  f1omo  47611