Theorem jaoi 856

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 850	. . 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 846

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 847

This theorem is referenced by:  jao1i  857  jaod  858  pm1.4  868  pm3.2ni  880  pm1.2  903  pm2.4  906  pm2.41  907  orim12i  908  pm1.5  919  pm2.42  942  jaoa  955  jaoian  956  pm4.44  996  andi  1007  ecase3  1031  cases2ALT  1048  consensus  1052  jaoi3  1060  1fpid3  1083  19.33  1891  19.33b  1892  nfim1  2201  dfsb2  2497  mooran1  2555  eueq3  3610  sbcor  3731  sspss  3990  sspsstr  3996  elun  4039  ssun  4079  inss  4129  raaan2  4411  ifbi  4436  ifcomnan  4470  elpr2OLD  4542  rabsnifsb  4613  tpprceq3  4692  tppreqb  4693  pwpw0  4701  sssn  4714  snsssn  4727  preq12b  4736  prnebg  4741  preq12nebg  4748  elpr2elpr  4754  pwsnOLD  4789  prproe  4794  3elpr2eq  4795  unissint  4860  zfpair  5288  propeqop  5364  propssopi  5365  opthhausdorff  5374  opthhausdorff0  5375  iunopeqop  5378  relsnb  5646  iresn0n0  5897  sotri2  5963  sotri3  5964  somincom  5968  ordssun  6271  unizlim  6289  onxpdisj  6292  tpres  6973  sorpssuni  7476  ordeleqon  7522  ordunisuc  7566  orduninsuc  7577  tfinds  7593  limomss  7604  limom  7614  soxp  7849  ressuppssdif  7880  tfr2b  8061  omopthi  8315  domnsym  8693  brwdom  9104  cantnfvalf  9201  djuss  9422  djuunxp  9423  eldju2ndl  9426  eldju2ndr  9427  djuun  9428  updjud  9436  iscard3  9593  cflim2  9763  sornom  9777  isfin5  9799  isfin6  9800  sdom2en01  9802  fin23lem29  9841  fin23lem30  9842  fin56  9893  fin67  9895  hsmexlem9  9925  axcc4dom  9941  axdc3lem2  9951  axdc3lem4  9953  brdom3  10028  winainflem  10193  r1tskina  10282  indpi  10407  ltxrlt  10789  nn0sub  12026  nn0n0n1ge2b  12044  nn0ge2m1nn  12045  xnn0xr  12053  xnn0nemnf  12059  elnn0z  12075  nn0lt10b  12125  nn0le2is012  12127  nn0ind-raph  12163  uzin  12360  indstr2  12409  nn0ledivnn  12585  xrnemnf  12595  xrnepnf  12596  mnfltxr  12605  xnn0n0n1ge2b  12609  xnn0ge0  12611  xnn0xaddcl  12711  xnn0lenn0nn0  12721  xnn0xadd0  12723  xmullem2  12741  rexmul  12747  xnn0xrge0  12980  elfzonlteqm1  13204  elfznelfzo  13233  injresinjlem  13248  injresinj  13249  fldiv4p1lem1div2  13296  fldiv4lem1div2  13298  modfzo0difsn  13402  ssnn0fi  13444  fsuppmapnn0fiubex  13451  m1expcl2  13543  m1expeven  13568  sq01  13678  expnngt1  13694  nn0opthi  13722  facp1  13730  faclbnd3  13744  faclbnd4lem1  13745  faclbnd4lem3  13747  bcn1  13765  hashnemnf  13796  hashv01gt1  13797  hashneq0  13817  hashrabrsn  13825  hashrabsn01  13826  hashrabsn1  13827  hashunx  13839  hashsnle1  13870  hashfzp1  13884  hash2pwpr  13928  hashge2el2difr  13933  swrdnd2  14106  pfxnd0  14139  repswswrd  14235  relexpsucl  14480  relexpsucr  14481  relexpcnv  14484  relexprelg  14487  relexpdmg  14491  relexprng  14495  relexpfld  14498  relexpaddg  14502  sumz  15172  arisum  15308  arisum2  15309  pwdif  15316  ntrivcvg  15345  prod1  15390  fprodfac  15419  mod2eq1n2dvds  15792  mulsucdiv2z  15798  nn0o1gt2  15826  nno  15827  nn0o  15828  sumeven  15832  sumodd  15833  divalglem1  15839  divalglem6  15843  gcdaddmlem  15967  dfgcd2  15990  mulgcd  15992  lcmf  16074  lcmfunsnlem2lem2  16080  lcmfunsnlem2  16081  prm2orodd  16132  dfphi2  16211  nnnn0modprm0  16243  prm23lt5  16251  oddprmdvds  16339  4sqlem19  16399  ramz  16461  prmolefac  16482  prmgaplem7  16493  cshwshashlem1  16532  ressval3d  16664  firest  16809  xpsfeq  16939  funcres2c  17276  smndex1basss  18186  smndex1mgm  18188  smndex1mndlem  18190  mulgnn0gsum  18352  symgfix2  18662  pmtrprfval  18733  m1expaddsub  18744  psgnprfval  18767  gsumpr  19194  gsumzunsnd  19195  sralem  20068  0ringnnzr  20161  frgpcyg  20392  cnmsgnsubg  20393  psgninv  20398  zrhpsgnelbas  20410  m2detleiblem1  21375  symgmatr01lem  21404  indiscld  21842  pnfnei  21971  mnfnei  21972  alexsubALTlem2  22799  alexsubALTlem3  22800  dscmet  23325  xrtgioo  23558  ishl2  24122  iunmbl2  24309  icombl  24316  ioombl  24317  recnprss  24656  recnperf  24657  dvexp2  24706  dvexp3  24730  dvne0f1  24764  plypf1  24961  taylfvallem1  25104  taylfval  25106  tayl0  25109  coseq0negpitopi  25248  logfac  25344  cxpexp  25411  pythag  25555  reasinsin  25634  harmonicbnd3  25745  lgslem4  26036  gausslemma2dlem0i  26100  lgsquadlem2  26117  2lgslem3  26140  2lgs  26143  2lgsoddprmlem3  26150  2sqnn0  26174  2sqnn  26175  cchhllem  26833  lfgrnloop  27070  uhgr2edg  27150  usgredg4  27159  usgredg2v  27169  usgrexmplef  27201  nb3grprlem1  27322  uvtx01vtx  27339  wlk1walk  27580  upgriswlk  27582  pthdadjvtx  27671  upgrwlkdvdelem  27677  pthdlem2lem  27708  2pthon3v  27881  clwwlkn  27963  clwwlkneq0  27966  eupth2lem3lem4  28168  konigsberg  28194  3vfriswmgrlem  28214  1to2vfriswmgr  28216  1to3vfriswmgr  28217  frgrregorufr0  28261  numclwlk1  28308  ex-pr  28367  shunssi  29303  cvmdi  30259  1neg1t1neg1  30647  iundisj2cnt  30695  fz1nnct  30699  xrge0iifiso  31457  esumpr2  31605  measiuns  31755  sxbrsigalem0  31808  bnj964  32494  subfacval3  32722  kur14lem7  32745  satfrnmapom  32903  gonar  32928  goalr  32930  mrsubcv  33043  nepss  33235  fz0n  33267  bccolsum  33276  dfon2lem7  33337  trpredlem1  33369  trpred0  33378  sltres  33506  nolesgn2o  33515  nogesgn1o  33517  nosep1o  33525  nosep2o  33526  noetalem2  33586  ssltun1  33643  ssltun2  33644  altopthsn  33901  elhf2  34115  nn0prpw  34150  dissym1  34248  ordcmp  34274  bj-currypeirce  34375  bj-jaoi1  34390  bj-jaoi2  34391  bj-ififc  34401  bj-andnotim  34408  bj-nfimexal  34445  bj-sbsb  34651  bj-elsn12g  34854  bj-ideqg1  34956  finxpreclem2  35184  wl-equsal1i  35325  tan2h  35392  poimirlem23  35423  poimirlem32  35432  itg2addnclem  35451  orfa1  35866  orfa2  35867  imaexALTV  36088  inex3  36096  inxpex  36097  elpadd0  37446  sbor2  39768  sn-0ne2  39966  sn-0lt1  40009  hbtlem5  40525  rp-fakeimass  40673  rp-isfinite6  40679  pr2cv  40700  iunrelexp0  40856  relexpss1d  40859  relexpmulg  40864  iunrelexpmin2  40866  relexp01min  40867  relexp0a  40870  relexpxpmin  40871  relexpaddss  40872  clsk1indlem3  41199  ssrecnpr  41464  seff  41465  sblpnf  41466  expgrowthi  41489  dvconstbi  41490  19.33-2  41538  ax6e2ndeq  41717  en3lpVD  42003  undif3VD  42040  ax6e2ndeqVD  42067  ax6e2ndeqALT  42089  iooinlbub  42579  elprneb  44062  euoreqb  44134  2reu3  44135  afvpcfv0  44171  afvfv0bi  44177  afvco2  44201  afv2orxorb  44253  afv2ndeffv0  44285  afv2fv0b  44291  fvmptrabdm  44318  iccpartltu  44411  iccpartgtl  44412  iccpartgt  44413  iccpartleu  44414  iccpartgel  44415  iccpartnel  44424  elsprel  44461  prsprel  44473  sprsymrelfolem2  44479  paireqne  44497  odz2prm2pw  44549  fmtnofac1  44556  fmtno4prmfac  44558  31prm  44583  lighneallem2  44592  lighneallem3  44593  lighneallem4b  44595  lighneallem4  44596  zeo2ALTV  44657  nn0o1gt2ALTV  44680  nn0oALTV  44682  stgoldbwt  44762  sbgoldbwt  44763  sbgoldbalt  44767  sbgoldbm  44770  sbgoldbo  44773  nnsum3primesle9  44780  nnsum4primeseven  44786  nnsum4primesevenALTV  44787  wtgoldbnnsum4prm  44788  bgoldbnnsum3prm  44790  bgoldbtbndlem1  44791  bgoldbtbnd  44795  tgoldbach  44803  isomuspgrlem1  44813  upgrwlkupwlk  44836  ztprmneprm  45217  islinindfis  45324  lindslinindsimp2lem5  45337  lindslinindsimp2  45338  lindsrng01  45343  elfzolborelfzop1  45394  flnn0div2ge  45413  blennn0elnn  45457  blen1b  45468  nnolog2flm1  45470  blengt1fldiv2p1  45473  0dig2pr01  45490  dignn0flhalf  45498  nn0sumshdiglemB  45500  nn0sumshdiglem1  45501  resum2sqorgt0  45589  rrx2xpref1o  45598  rrx2plord2  45602  itsclc0yqsol  45644  mosssn  45692  mo0sn  45693  mofsssn  45703  mofmo  45704  f1omo  45711