MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  jaoi Unicode version

Theorem jaoi 369
Description: Inference disjoining the antecedents of two implications. (Contributed by NM, 5-Apr-1994.)
Hypotheses
Ref Expression
jaoi.1  |-  ( ph  ->  ps )
jaoi.2  |-  ( ch 
->  ps )
Assertion
Ref Expression
jaoi  |-  ( (
ph  \/  ch )  ->  ps )

Proof of Theorem jaoi
StepHypRef Expression
1 pm2.53 363 . . 3  |-  ( (
ph  \/  ch )  ->  ( -.  ph  ->  ch ) )
2 jaoi.2 . . 3  |-  ( ch 
->  ps )
31, 2syl6 31 . 2  |-  ( (
ph  \/  ch )  ->  ( -.  ph  ->  ps ) )
4 jaoi.1 . 2  |-  ( ph  ->  ps )
53, 4pm2.61d2 154 1  |-  ( (
ph  \/  ch )  ->  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 358
This theorem is referenced by:  jaod  370  pm1.4  376  jaoa  497  pm1.2  500  orim12i  503  pm1.5  509  pm2.41  557  pm2.42  558  pm2.4  559  pm4.44  561  jaoian  760  pm2.64  765  pm2.82  826  pm3.2ni  828  andi  838  ecase3  908  consensus  926  cad1  1407  19.33  1617  19.33b  1618  dfsb2  2115  mooran1  2334  2eu3  2362  eueq3  3101  sbcor  3197  sspss  3438  sspsstr  3444  elun  3480  ssun  3518  inss  3562  undif3  3594  ifbi  3748  elpr2  3825  tpprceq3  3930  tppreqb  3931  pwpw0  3938  sssn  3949  snsssn  3959  preq12b  3966  prnebg  3971  pwsnALT  4002  unissint  4066  zfpair  4393  ordelinel  4671  ordssun  4672  ordequn  4673  onun2i  4688  unizlim  4689  reusv6OLD  4725  reusv7OLD  4726  ordeleqon  4760  ordunisuc  4803  orduninsuc  4814  tfinds  4830  limomss  4841  limom  4851  onxpdisj  4948  sotri2  5254  sotri3  5255  somincom  5262  funtpg  5492  fvfundmfvn0  5753  bropopvvv  6417  soxp  6450  sorpssuni  6522  sorpssint  6523  tfr2b  6648  omopthi  6891  domnsym  7224  brwdom  7524  cantnfvalf  7609  iscard3  7963  cflim2  8132  sornom  8146  isfin5  8168  isfin6  8169  sdom2en01  8171  fin23lem29  8210  fin23lem30  8211  fin56  8262  fin67  8264  hsmexlem9  8294  axcc4dom  8310  axdc3lem2  8320  axdc3lem4  8322  brdom3  8395  winainflem  8557  r1tskina  8646  indpi  8773  renfdisj  9127  ltxrlt  9135  ltlen  9164  elnnnn0b  10253  nn0sub  10259  nn0n0n1ge2b  10270  elnn0z  10283  nn0ind-raph  10359  uzin  10507  indstr2  10543  xrnemnf  10707  xrnepnf  10708  mnfltxr  10713  nn0pnfge0  10717  xmullem2  10833  rexmul  10839  elfznelfzo  11180  injresinjlem  11187  injresinj  11188  m1expcl2  11391  sq01  11489  nn0opthi  11551  facp1  11559  faclbnd3  11571  faclbnd4lem1  11572  faclbnd4lem3  11574  bcn1  11592  hashnemnf  11616  hashv01gt1  11617  hashrabrsn  11636  hashunx  11648  sumz  12504  arisum  12627  arisum2  12628  divalglem1  12902  divalglem6  12906  gcdaddmlem  13016  mulgcd  13034  dfphi2  13151  4sqlem19  13319  ramz  13381  firest  13648  xpsfeq  13777  xpsfrnel2  13778  funcres2c  14086  sralem  16237  prmirred  16763  frgpcyg  16842  indiscld  17143  pnfnei  17272  mnfnei  17273  alexsubALTlem2  18067  alexsubALTlem3  18068  dscmet  18608  xrtgioo  18825  ishl2  19312  iunmbl2  19439  icombl  19446  ioombl  19447  recnprss  19779  recnperf  19780  dvexp2  19828  dvexp3  19850  dvne0f1  19884  plypf1  20119  taylfvallem1  20261  taylfval  20263  tayl0  20266  coseq0negpitopi  20399  logfac  20483  cxpexp  20547  pythag  20647  reasinsin  20724  harmonicbnd3  20834  lgslem4  21071  lgsquadlem2  21127  usgraedgprv  21384  usgraedgrnv  21385  usgraedg4  21394  usgraidx2v  21400  usgraexmpl  21408  nb3graprlem1  21448  wlkdvspthlem  21595  constr3trllem2  21626  vdgrf  21657  konigsberg  21697  ex-pr  21726  shunssi  22858  cvmdi  23815  iundisj2cnt  24143  xrge0iifiso  24309  esumpr2  24446  measiuns  24559  sxbrsigalem0  24609  subfacval3  24863  kur14lem7  24886  m1expevenALT  24893  nepss  25163  fz0n  25190  ntrivcvg  25214  prod1  25259  fprodfac  25285  dfon2lem7  25400  trpredlem1  25485  trpred0  25494  sltres  25573  altopthsn  25754  axlowdimlem15  25843  elhf2  26064  dissym1  26119  ordcmp  26145  itg2addnclem  26202  nn0prpw  26263  prtlem1  26627  hbtlem5  27247  m1expaddsub  27336  cnmsgnsubg  27349  ssrecnpr  27452  seff  27453  sblpnf  27454  expgrowthi  27465  dvconstbi  27466  19.33-2  27495  raaan2  27867  2reu3  27880  afvpcfv0  27924  afvfv0bi  27930  afvco2  27954  swrdnd  28074  usgra2wlkspthlem1  28180  usgra2adedgspthlem2  28188  2wlkonot3v  28216  2spthonot3v  28217  3vfriswmgralem  28252  1to2vfriswmgra  28254  1to3vfriswmgra  28255  vdgfrgragt2  28276  frgrawopreglem2  28292  frgrawopreglem3  28293  frgraregorufr0  28299  a9e2ndeq  28501  en3lpVD  28811  undif3VD  28848  a9e2ndeqVD  28875  a9e2ndeqALT  28898  bnj964  29168  dfsb2NEW7  29487  elpadd0  30445
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-or 360
  Copyright terms: Public domain W3C validator