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  2491  mooran1  2548  eueq3  3672  sbcor  3795  sspss  4064  sspsstr  4070  elun  4113  ssun  4154  inss  4203  raaan2  4487  ifbi  4513  ifcomnan  4547  elpr2OLD  4617  rabsnifsb  4688  tpprceq3  4769  tppreqb  4770  pwpw0  4778  sssn  4791  snsssn  4804  preq12b  4813  prnebg  4818  preq12nebg  4825  elpr2elpr  4831  pwsnOLD  4863  prproe  4868  3elpr2eq  4869  unissint  4938  zfpair  5381  propeqop  5469  propssopi  5470  opthhausdorff  5479  opthhausdorff0  5480  iunopeqop  5483  relsnb  5763  iresn0n0  6012  sotri2  6088  sotri3  6089  somincom  6093  ordssun  6424  unizlim  6445  onxpdisj  6448  tpres  7155  sorpssuni  7674  ordeleqon  7721  ordunisuc  7772  orduninsuc  7784  tfinds  7801  limomss  7812  limom  7823  soxp  8066  ressuppssdif  8121  tfr2b  8347  omopthi  8612  domnsym  9050  brwdom  9512  cantnfvalf  9610  ttrclselem1  9670  djuss  9865  djuunxp  9866  eldju2ndl  9869  eldju2ndr  9870  djuun  9871  updjud  9879  iscard3  10038  cflim2  10208  sornom  10222  isfin5  10244  isfin6  10245  sdom2en01  10247  fin23lem29  10286  fin23lem30  10287  fin56  10338  fin67  10340  hsmexlem9  10370  axcc4dom  10386  axdc3lem2  10396  axdc3lem4  10398  brdom3  10473  winainflem  10638  r1tskina  10727  indpi  10852  ltxrlt  11234  nn0sub  12472  nn0n0n1ge2b  12490  nn0ge2m1nn  12491  xnn0xr  12499  xnn0nemnf  12505  elnn0z  12521  nn0lt10b  12574  nn0le2is012  12576  nn0ind-raph  12612  uzin  12812  indstr2  12861  nn0ledivnn  13037  xrnemnf  13047  xrnepnf  13048  mnfltxr  13057  xnn0n0n1ge2b  13061  xnn0ge0  13063  xnn0xaddcl  13164  xnn0lenn0nn0  13174  xnn0xadd0  13176  xmullem2  13194  rexmul  13200  xnn0xrge0  13433  elfzonlteqm1  13658  elfznelfzo  13687  injresinjlem  13702  injresinj  13703  fldiv4p1lem1div2  13750  fldiv4lem1div2  13752  modfzo0difsn  13858  ssnn0fi  13900  fsuppmapnn0fiubex  13907  m1expcl2  14001  m1expeven  14025  zzlesq  14120  sq01  14138  expnngt1  14154  nn0opthi  14180  facp1  14188  faclbnd3  14202  faclbnd4lem1  14203  faclbnd4lem3  14205  bcn1  14223  hashnemnf  14254  hashv01gt1  14255  hashneq0  14274  hashrabrsn  14282  hashrabsn01  14283  hashrabsn1  14284  hashunx  14296  hashsnle1  14327  hashfzp1  14341  hash2pwpr  14387  hashge2el2difr  14392  swrdnd2  14555  pfxnd0  14588  repswswrd  14684  relexpsucl  14928  relexpsucr  14929  relexpcnv  14932  relexprelg  14935  relexpdmg  14939  relexprng  14943  relexpfld  14946  relexpaddg  14950  sumz  15618  arisum  15756  arisum2  15757  pwdif  15764  ntrivcvg  15793  prod1  15838  fprodfac  15867  mod2eq1n2dvds  16240  mulsucdiv2z  16246  nn0o1gt2  16274  nno  16275  nn0o  16276  sumeven  16280  sumodd  16281  divalglem1  16287  divalglem6  16291  gcdaddmlem  16415  dfgcd2  16438  mulgcd  16440  lcmf  16520  lcmfunsnlem2lem2  16526  lcmfunsnlem2  16527  prm2orodd  16578  dfphi2  16657  nnnn0modprm0  16689  prm23lt5  16697  oddprmdvds  16786  4sqlem19  16846  ramz  16908  prmolefac  16929  prmgaplem7  16940  cshwshashlem1  16979  ressval3d  17141  ressval3dOLD  17142  firest  17328  xpsfeq  17459  funcres2c  17802  smndex1basss  18729  smndex1mgm  18731  smndex1mndlem  18733  mulgnn0gsum  18896  symgfix2  19212  pmtrprfval  19283  m1expaddsub  19294  psgnprfval  19317  gsumpr  19746  gsumzunsnd  19747  0ringnnzr  20212  sralemOLD  20698  frgpcyg  21017  cnmsgnsubg  21018  psgninv  21023  zrhpsgnelbas  21035  m2detleiblem1  22010  symgmatr01lem  22039  indiscld  22479  pnfnei  22608  mnfnei  22609  alexsubALTlem2  23436  alexsubALTlem3  23437  dscmet  23965  xrtgioo  24206  ishl2  24771  iunmbl2  24958  icombl  24965  ioombl  24966  recnprss  25305  recnperf  25306  dvexp2  25355  dvexp3  25379  dvne0f1  25413  plypf1  25610  taylfvallem1  25753  taylfval  25755  tayl0  25758  coseq0negpitopi  25897  logfac  25993  cxpexp  26060  pythag  26204  reasinsin  26283  harmonicbnd3  26394  lgslem4  26685  gausslemma2dlem0i  26749  lgsquadlem2  26766  2lgslem3  26789  2lgs  26792  2lgsoddprmlem3  26799  2sqnn0  26823  2sqnn  26824  sltres  27047  nolesgn2o  27056  nogesgn1o  27058  nosep1o  27066  nosep2o  27067  noetalem2  27127  ssltun1  27190  ssltun2  27191  cchhllemOLD  27899  lfgrnloop  28139  uhgr2edg  28219  usgredg4  28228  usgredg2v  28238  usgrexmplef  28270  nb3grprlem1  28391  uvtx01vtx  28408  wlk1walk  28650  upgriswlk  28652  pthdadjvtx  28741  upgrwlkdvdelem  28747  pthdlem2lem  28778  2pthon3v  28951  clwwlkn  29033  clwwlkneq0  29036  eupth2lem3lem4  29238  konigsberg  29264  3vfriswmgrlem  29284  1to2vfriswmgr  29286  1to3vfriswmgr  29287  frgrregorufr0  29331  numclwlk1  29378  ex-pr  29437  shunssi  30373  cvmdi  31329  1neg1t1neg1  31722  iundisj2cnt  31770  fz1nnct  31774  xrge0iifiso  32605  esumpr2  32755  measiuns  32905  sxbrsigalem0  32960  bnj964  33644  subfacval3  33870  kur14lem7  33893  satfrnmapom  34051  gonar  34076  goalr  34078  mrsubcv  34191  nepss  34376  nnuni  34385  fz0n  34389  bccolsum  34398  dfon2lem7  34450  altopthsn  34622  elhf2  34836  nn0prpw  34871  dissym1  34969  ordcmp  34995  bj-currypeirce  35096  bj-jaoi1  35111  bj-jaoi2  35112  bj-ififc  35122  bj-andnotim  35129  bj-nfimexal  35166  bj-sbsb  35378  bj-elsn12g  35604  bj-ideqg1  35708  finxpreclem2  35934  wl-equsal1i  36075  tan2h  36143  poimirlem23  36174  poimirlem32  36183  itg2addnclem  36202  orfa1  36617  orfa2  36618  imaexALTV  36864  inex3  36872  inxpex  36873  mopickr  36897  disjlem14  37333  elpadd0  38345  aks6d1c2p2  40622  sbor2  40702  sn-0ne2  40933  sn-0lt1  40989  hbtlem5  41513  omabs2  41725  safesnsupfiss  41809  safesnsupfidom1o  41811  safesnsupfilb  41812  rp-fakeimass  41906  rp-isfinite6  41912  pr2cv  41942  iunrelexp0  42096  relexpss1d  42099  relexpmulg  42104  iunrelexpmin2  42106  relexp01min  42107  relexp0a  42110  relexpxpmin  42111  relexpaddss  42112  clsk1indlem3  42437  ssrecnpr  42710  seff  42711  sblpnf  42712  expgrowthi  42735  dvconstbi  42736  19.33-2  42784  ax6e2ndeq  42963  en3lpVD  43249  undif3VD  43286  ax6e2ndeqVD  43313  ax6e2ndeqALT  43335  iooinlbub  43859  elprneb  45383  euoreqb  45461  2reu3  45462  afvpcfv0  45498  afvfv0bi  45504  afvco2  45528  afv2orxorb  45580  afv2ndeffv0  45612  afv2fv0b  45618  fvmptrabdm  45645  iccpartltu  45737  iccpartgtl  45738  iccpartgt  45739  iccpartleu  45740  iccpartgel  45741  iccpartnel  45750  elsprel  45787  prsprel  45799  sprsymrelfolem2  45805  paireqne  45823  odz2prm2pw  45875  fmtnofac1  45882  fmtno4prmfac  45884  31prm  45909  lighneallem2  45918  lighneallem3  45919  lighneallem4b  45921  lighneallem4  45922  zeo2ALTV  45983  nn0o1gt2ALTV  46006  nn0oALTV  46008  stgoldbwt  46088  sbgoldbwt  46089  sbgoldbalt  46093  sbgoldbm  46096  sbgoldbo  46099  nnsum3primesle9  46106  nnsum4primeseven  46112  nnsum4primesevenALTV  46113  wtgoldbnnsum4prm  46114  bgoldbnnsum3prm  46116  bgoldbtbndlem1  46117  bgoldbtbnd  46121  tgoldbach  46129  isomuspgrlem1  46139  upgrwlkupwlk  46162  ztprmneprm  46543  islinindfis  46650  lindslinindsimp2lem5  46663  lindslinindsimp2  46664  lindsrng01  46669  elfzolborelfzop1  46720  flnn0div2ge  46739  blennn0elnn  46783  blen1b  46794  nnolog2flm1  46796  blengt1fldiv2p1  46799  0dig2pr01  46816  dignn0flhalf  46824  nn0sumshdiglemB  46826  nn0sumshdiglem1  46827  resum2sqorgt0  46915  rrx2xpref1o  46924  rrx2plord2  46928  itsclc0yqsol  46970  mosssn  47019  mo0sn  47020  mofsssn  47032  mofmo  47033  f1omo  47047