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  1404  19.33  1614  19.33b  1615  dfsb2  2104  mooran1  2308  2eu3  2336  eueq3  3069  sbcor  3165  sspss  3406  sspsstr  3412  elun  3448  ssun  3486  inss  3530  undif3  3562  ifbi  3716  elpr2  3793  tpprceq3  3898  tppreqb  3899  pwpw0  3906  sssn  3917  snsssn  3927  preq12b  3934  prnebg  3939  pwsnALT  3970  unissint  4034  zfpair  4361  ordelinel  4639  ordssun  4640  ordequn  4641  onun2i  4656  unizlim  4657  reusv6OLD  4693  reusv7OLD  4694  ordeleqon  4728  ordunisuc  4771  orduninsuc  4782  tfinds  4798  limomss  4809  limom  4819  onxpdisj  4916  sotri2  5222  sotri3  5223  somincom  5230  funtpg  5460  fvfundmfvn0  5721  bropopvvv  6385  soxp  6418  sorpssuni  6490  sorpssint  6491  tfr2b  6616  omopthi  6859  domnsym  7192  brwdom  7491  cantnfvalf  7576  iscard3  7930  cflim2  8099  sornom  8113  isfin5  8135  isfin6  8136  sdom2en01  8138  fin23lem29  8177  fin23lem30  8178  fin56  8229  fin67  8231  hsmexlem9  8261  axcc4dom  8277  axdc3lem2  8287  axdc3lem4  8289  brdom3  8362  winainflem  8524  r1tskina  8613  indpi  8740  renfdisj  9094  ltxrlt  9102  ltlen  9131  elnnnn0b  10220  nn0sub  10226  nn0n0n1ge2b  10237  elnn0z  10250  nn0ind-raph  10326  uzin  10474  indstr2  10510  xrnemnf  10674  xrnepnf  10675  mnfltxr  10680  nn0pnfge0  10684  xmullem2  10800  rexmul  10806  elfznelfzo  11147  injresinjlem  11154  injresinj  11155  m1expcl2  11358  sq01  11456  nn0opthi  11518  facp1  11526  faclbnd3  11538  faclbnd4lem1  11539  faclbnd4lem3  11541  bcn1  11559  hashnemnf  11583  hashv01gt1  11584  hashrabrsn  11603  hashunx  11615  sumz  12471  arisum  12594  arisum2  12595  divalglem1  12869  divalglem6  12873  gcdaddmlem  12983  mulgcd  13001  dfphi2  13118  4sqlem19  13286  ramz  13348  firest  13615  xpsfeq  13744  xpsfrnel2  13745  funcres2c  14053  sralem  16204  prmirred  16730  frgpcyg  16809  indiscld  17110  pnfnei  17238  mnfnei  17239  alexsubALTlem2  18032  alexsubALTlem3  18033  dscmet  18573  xrtgioo  18790  ishl2  19277  iunmbl2  19404  icombl  19411  ioombl  19412  recnprss  19744  recnperf  19745  dvexp2  19793  dvexp3  19815  dvne0f1  19849  plypf1  20084  taylfvallem1  20226  taylfval  20228  tayl0  20231  coseq0negpitopi  20364  logfac  20448  cxpexp  20512  pythag  20612  reasinsin  20689  harmonicbnd3  20799  lgslem4  21036  lgsquadlem2  21092  usgraedgprv  21349  usgraedgrnv  21350  usgraedg4  21359  usgraidx2v  21365  usgraexmpl  21373  nb3graprlem1  21413  wlkdvspthlem  21560  constr3trllem2  21591  vdgrf  21622  konigsberg  21662  ex-pr  21691  shunssi  22823  cvmdi  23780  iundisj2cnt  24108  xrge0iifiso  24274  esumpr2  24411  measiuns  24524  sxbrsigalem0  24574  subfacval3  24828  kur14lem7  24851  m1expevenALT  24858  nepss  25128  fz0n  25155  ntrivcvg  25178  prod1  25223  fprodfac  25249  dfon2lem7  25359  trpredlem1  25444  trpred0  25453  sltres  25532  altopthsn  25710  axlowdimlem15  25799  elhf2  26020  dissym1  26075  ordcmp  26101  itg2addnclem  26155  nn0prpw  26216  prtlem1  26580  hbtlem5  27200  m1expaddsub  27289  cnmsgnsubg  27302  ssrecnpr  27405  seff  27406  sblpnf  27407  expgrowthi  27418  dvconstbi  27419  19.33-2  27448  raaan2  27820  2reu3  27833  afvpcfv0  27877  afvfv0bi  27883  afvco2  27907  swrdnd  28001  usgra2wlkspthlem1  28036  usgra2adedgspthlem2  28044  2wlkonot3v  28072  2spthonot3v  28073  3vfriswmgralem  28108  1to2vfriswmgra  28110  1to3vfriswmgra  28111  vdgfrgragt2  28132  frgrawopreglem2  28148  frgrawopreglem3  28149  frgraregorufr0  28155  a9e2ndeq  28357  en3lpVD  28666  undif3VD  28703  a9e2ndeqVD  28730  a9e2ndeqALT  28753  bnj964  29020  dfsb2NEW7  29339  elpadd0  30291
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