Theorem jaoi 393

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

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

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 196  df-or 384

This theorem is referenced by:  jaod  394  pm1.4  400  jaoa  531  pm1.2  534  orim12i  537  pm1.5  543  pm2.41  595  pm2.42  596  pm2.4  597  pm4.44  599  jaoian  820  jao1i  821  pm3.2ni  895  andi  907  ecase3  979  consensus  990  jaoi3  1003  cases2  1005  1fpid3  1023  19.33  1801  19.33b  1802  19.40bOLD  1805  nfim1  2055  dfsb2  2361  mooran1  2515  2eu3  2543  eueq3  3348  sbcor  3446  sspss  3668  sspsstr  3674  elun  3715  ssun  3754  inss  3804  undif3OLD  3848  ifbi  4057  ifcomnan  4087  elpr2  4147  elpr2OLD  4148  eqoreldifOLD  4173  rabsnifsb  4201  tpprceq3  4276  tppreqb  4277  pwpw0  4284  sssn  4298  snsssn  4312  preq12b  4322  prnebg  4329  elpr2elpr  4336  pwsnALT  4367  unissint  4436  zfpair  4831  propeqop  4895  propssopi  4896  iunopeqop  4906  sotri2  5444  sotri3  5445  somincom  5449  ordelinelOLD  5743  ordssun  5744  onun2i  5760  unizlim  5761  onxpdisj  5764  funtpgOLD  5857  fvfundmfvn0  6136  tpres  6371  sorpssuni  6844  sorpssint  6845  ordeleqon  6880  ordunisuc  6924  orduninsuc  6935  tfinds  6951  limomss  6962  limom  6972  soxp  7177  ressuppssdif  7203  tfr2b  7379  omopthi  7624  domnsym  7971  brwdom  8355  cantnfvalf  8445  iscard3  8799  cflim2  8968  sornom  8982  isfin5  9004  isfin6  9005  sdom2en01  9007  fin23lem29  9046  fin23lem30  9047  fin56  9098  fin67  9100  hsmexlem9  9130  axcc4dom  9146  axdc3lem2  9156  axdc3lem4  9158  brdom3  9231  winainflem  9394  r1tskina  9483  indpi  9608  ltxrlt  9987  ltlen  10017  elnnnn0b  11214  nn0sub  11220  nn0n0n1ge2b  11236  nn0ge2m1nn  11237  xnn0xr  11245  xnn0nemnf  11251  elnn0z  11267  nn0lt10b  11316  nn0ind-raph  11353  znnn0nn  11365  uzin  11596  indstr2  11643  nn0ledivnn  11817  xrnemnf  11827  xrnepnf  11828  mnfltxr  11837  xnn0n0n1ge2b  11841  xnn0ge0  11843  nn0pnfge0OLD  11844  xnn0xaddcl  11940  xnn0xadd0  11949  xmullem2  11967  rexmul  11973  xnn0xrge0  12196  elfzonlteqm1  12410  elfznelfzo  12439  injresinjlem  12450  injresinj  12451  fldiv4p1lem1div2  12498  fldiv4lem1div2  12500  modfzo0difsn  12604  ssnn0fi  12646  fsuppmapnn0fiubex  12654  m1expcl2  12744  m1expeven  12769  sq01  12848  nn0opthi  12919  facp1  12927  faclbnd3  12941  faclbnd4lem1  12942  faclbnd4lem3  12944  bcn1  12962  hashnemnf  12994  hashv01gt1  12995  hashneq0  13016  hashrabrsn  13022  hashrabsn01  13023  hashrabsn1  13024  hashunx  13036  hashsnle1  13066  hashfzp1  13078  hash2pwpr  13115  hashge2el2difr  13118  swrdnd2  13285  repswswrd  13382  scshwfzeqfzo  13423  relexpsucr  13617  relexpsucl  13621  relexpcnv  13623  relexprelg  13626  relexpdmg  13630  relexprng  13634  relexpfld  13637  relexpaddg  13641  sumz  14300  arisum  14431  arisum2  14432  ntrivcvg  14468  prod1  14513  fprodfac  14542  mod2eq1n2dvds  14909  mulsucdiv2z  14915  nn0enne  14932  nn0o1gt2  14935  nno  14936  nn0o  14937  sumeven  14948  sumodd  14949  divalglem1  14955  divalglem6  14959  gcdaddmlem  15083  dfgcd2  15101  mulgcd  15103  lcmf  15184  lcmfunsnlem2lem2  15190  lcmfunsnlem2  15191  prm2orodd  15242  dfphi2  15317  nnnn0modprm0  15349  prm23lt5  15357  oddprmdvds  15445  4sqlem19  15505  ramz  15567  prmolefac  15588  prmgaplem7  15599  cshwshashlem1  15640  ressval3d  15764  firest  15916  xpsfeq  16047  xpsfrnel2  16048  funcres2c  16384  symgfix2  17659  pmtrprfval  17730  m1expaddsub  17741  psgnprfval  17764  gsumzunsnd  18178  sralem  18998  0ringnnzr  19090  prmirred  19662  frgpcyg  19741  cnmsgnsubg  19742  psgninv  19747  zrhpsgnelbas  19759  m2detleiblem1  20249  symgmatr01lem  20278  pmatcollpw3fi1  20412  indiscld  20705  pnfnei  20834  mnfnei  20835  alexsubALTlem2  21662  alexsubALTlem3  21663  dscmet  22187  xrtgioo  22417  ishl2  22974  iunmbl2  23132  icombl  23139  ioombl  23140  recnprss  23474  recnperf  23475  dvexp2  23523  dvexp3  23545  dvne0f1  23579  plypf1  23772  taylfvallem1  23915  taylfval  23917  tayl0  23920  coseq0negpitopi  24059  logfac  24151  cxpexp  24214  pythag  24347  reasinsin  24423  harmonicbnd3  24534  lgslem4  24825  gausslemma2dlem0i  24889  lgsquadlem2  24906  2lgslem3  24929  2lgs  24932  2lgsoddprmlem3  24939  cchhllem  25567  lfgrnloop  25791  usgraedgprv  25905  usgraedgrnv  25906  usgraedg4  25916  usgraidx2v  25922  usgraexmplef  25929  nb3graprlem1  25980  wlkdvspthlem  26137  usgra2adedgspthlem2  26140  usgra2wlkspthlem1  26147  constr3trllem2  26179  clwwlkgt0  26299  clwwlknprop  26300  vdgrf  26425  rusgrasn  26472  clwlknclwlkdifs  26487  konigsberg  26514  3vfriswmgralem  26531  1to2vfriswmgra  26533  1to3vfriswmgra  26534  vdgfrgragt2  26554  frgrawopreglem2  26572  frgrawopreglem3  26573  frgraregorufr0  26579  ex-pr  26679  shunssi  27611  cvmdi  28567  1neg1t1neg1  28902  iundisj2cnt  28945  fz1nnct  28947  xrge0iifiso  29309  esumpr2  29456  measiuns  29607  sxbrsigalem0  29660  bnj964  30267  subfacval3  30425  kur14lem7  30448  mrsubcv  30661  nepss  30854  fz0n  30869  bccolsum  30878  dfon2lem7  30938  trpredlem1  30971  trpred0  30980  sltres  31061  altopthsn  31238  elhf2  31452  nn0prpw  31488  dissym1  31590  ordcmp  31616  bj-jaoi1  31726  bj-jaoi2  31727  bj-andnotim  31746  bj-sbsb  32012  finxpreclem2  32403  wl-equsal1i  32508  tan2h  32571  poimirlem23  32602  poimirlem32  32611  itg2addnclem  32631  orfa1  33056  orfa2  33057  elpadd0  34113  hbtlem5  36717  rp-fakeimass  36876  rp-isfinite6  36883  iunrelexp0  37013  relexpss1d  37016  relexpmulg  37021  iunrelexpmin2  37023  relexp01min  37024  relexp0a  37027  relexpxpmin  37028  relexpaddss  37029  clsk1indlem3  37361  ssrecnpr  37529  seff  37530  sblpnf  37531  expgrowthi  37554  dvconstbi  37555  19.33-2  37603  ax6e2ndeq  37796  en3lpVD  38102  undif3VD  38140  ax6e2ndeqVD  38167  ax6e2ndeqALT  38189  iooinlbub  38570  raaan2  39824  2reu3  39837  afvpcfv0  39875  afvfv0bi  39881  afvco2  39905  elprneb  39939  iccpartltu  39963  iccpartgtl  39964  iccpartgt  39965  iccpartleu  39966  iccpartgel  39967  iccpartnel  39976  odz2prm2pw  40013  fmtnofac1  40020  fmtno4prmfac  40022  pwdif  40039  31prm  40050  lighneallem2  40061  lighneallem3  40062  lighneallem4b  40064  lighneallem4  40065  zeo2ALTV  40120  nn0o1gt2ALTV  40143  nn0oALTV  40145  stgoldbwt  40198  bgoldbwt  40199  sgoldbalt  40203  nnsum3primesle9  40210  nnsum4primeseven  40216  nnsum4primesevenALTV  40217  wtgoldbnnsum4prm  40218  bgoldbnnsum3prm  40220  bgoldbtbndlem1  40221  bgoldbtbnd  40225  tgoldbach  40232  tgoldbachOLD  40239  uhgr2edg  40435  usgredg4  40444  usgredg2v  40454  nb3grprlem1  40608  uvtxa01vtx0  40623  1wlk1walk  40843  upgr1wlkwlk  40847  pthdadjvtx  40936  upgrwlkdvdelem  40942  pthdlem2lem  40973  2pthon3v-av  41150  clwwlknclwwlkdifs  41181  eupth2lem3lem4  41399  konigsberg-av  41427  3vfriswmgrlem  41447  1to2vfriswmgr  41449  1to3vfriswmgr  41450  frgrwopreglem3  41483  frgrregorufr0  41489  av-numclwwlkffin0  41513  ztprmneprm  41918  gsumpr  41932  nn0le2is012  41938  islinindfis  42032  lindslinindsimp2lem5  42045  lindslinindsimp2  42046  lindsrng01  42051  elfzolborelfzop1  42103  flnn0div2ge  42121  blennn0elnn  42169  blen1b  42180  nnolog2flm1  42182  blengt1fldiv2p1  42185  0dig2pr01  42202  dignn0flhalf  42210  nn0sumshdiglemB  42212  nn0sumshdiglem1  42213