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

Theorem jaoi 368
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 362 . . 3  |-  ( (
ph  \/  ch )  ->  ( -.  ph  ->  ch ) )
2 jaoi.2 . . 3  |-  ( ch 
->  ps )
31, 2syl6 29 . 2  |-  ( (
ph  \/  ch )  ->  ( -.  ph  ->  ps ) )
4 jaoi.1 . 2  |-  ( ph  ->  ps )
53, 4pm2.61d2 152 1  |-  ( (
ph  \/  ch )  ->  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 357
This theorem is referenced by:  jaod  369  pm1.4  375  jaoa  496  pm1.2  499  orim12i  502  pm1.5  508  pm2.41  556  pm2.42  557  pm2.4  558  pm4.44  560  jaoian  759  pm2.64  764  pm2.82  825  pm3.2ni  827  andi  837  ecase3  907  consensus  925  cad1  1388  19.33  1594  19.33b  1595  dfsb2  1995  mooran1  2197  2eu3  2225  eueq3  2940  sbcor  3035  sspss  3275  sspsstr  3281  elun  3316  ssun  3354  inss  3398  undif3  3429  ifbi  3582  elpr2  3659  pwpw0  3763  sssn  3772  snsssn  3781  preq12b  3788  pwsnALT  3822  unissint  3886  zfpair  4212  pwundifOLD  4301  ordelinel  4491  ordssun  4492  ordequn  4493  onun2i  4508  unizlim  4509  reusv6OLD  4545  reusv7OLD  4546  ordeleqon  4580  ordunisuc  4623  orduninsuc  4634  tfinds  4650  limomss  4661  limom  4671  onxpdisj  4769  sotri2  5072  sotri3  5073  somincom  5080  soxp  6228  sorpssuni  6286  sorpssint  6287  tfr2b  6412  omopthi  6655  domnsym  6987  brwdom  7281  cantnfvalf  7366  iscard3  7720  cflim2  7889  sornom  7903  isfin5  7925  isfin6  7926  sdom2en01  7928  fin23lem29  7967  fin23lem30  7968  fin56  8019  fin67  8021  hsmexlem9  8051  axcc4dom  8067  axdc3lem2  8077  axdc3lem4  8079  brdom3  8153  winainflem  8315  r1tskina  8404  indpi  8531  renfdisj  8885  ltxrlt  8893  ltlen  8922  elnnnn0b  10008  nn0sub  10014  elnn0z  10036  nn0ind-raph  10112  uzin  10260  indstr2  10296  xrnemnf  10460  xrnepnf  10461  mnfltxr  10466  xmullem2  10585  rexmul  10591  m1expcl2  11125  sq01  11223  nn0opthi  11285  facp1  11293  faclbnd3  11305  faclbnd4lem1  11306  faclbnd4lem3  11308  bcn1  11325  sumz  12195  arisum  12318  arisum2  12319  divalglem1  12593  divalglem6  12597  gcdaddmlem  12707  mulgcd  12725  dfphi2  12842  4sqlem19  13010  ramz  13072  firest  13337  xpsfeq  13466  xpsfrnel2  13467  funcres2c  13775  sralem  15930  prmirred  16448  frgpcyg  16527  indiscld  16828  pnfnei  16950  mnfnei  16951  alexsubALTlem2  17742  alexsubALTlem3  17743  dscmet  18095  xrtgioo  18312  ishl2  18787  iunmbl2  18914  icombl  18921  ioombl  18922  recnprss  19254  recnperf  19255  dvexp2  19303  dvexp3  19325  dvne0f1  19359  plypf1  19594  taylfvallem1  19736  taylfval  19738  tayl0  19741  coseq0negpitopi  19871  logfac  19954  cxpexp  20015  pythag  20115  reasinsin  20192  harmonicbnd3  20301  lgslem4  20538  lgsquadlem2  20594  ex-pr  20817  shunssi  21947  cvmdi  22904  xrge0iifiso  23317  iundisj2cnt  23368  esumpr2  23439  measiuns  23544  subfacval3  23720  kur14lem7  23743  konigsberg  23911  nepss  24072  fz0n  24097  dfon2lem7  24145  trpredlem1  24230  trpred0  24239  sltres  24318  altopthsn  24495  axlowdimlem15  24584  elhf2  24805  dissym1  24860  ordcmp  24886  facrm  24953  nxtor  24985  untindd  25019  neiopne  25051  cbcpcp  25162  tolat  25286  basexre  25522  cntrset  25602  intvconlem1  25703  vtarsuelt  25895  inttarcar  25901  fnckle  26045  pfsubkl  26047  pdiveql  26168  nn0prpw  26239  prtlem1  26707  hbtlem5  27332  m1expaddsub  27421  cnmsgnsubg  27434  ssrecnpr  27537  seff  27538  sblpnf  27539  expgrowthi  27550  dvconstbi  27551  19.33-2  27580  raaan2  27953  2reu3  27966  fvfundmfvn0  27986  afvpcfv0  28009  afvfv0bi  28015  afvco2  28037  tpprceq3  28072  usgraedgprv  28122  usgraedgrnv  28123  usgraexmpl  28133  3vfriswmgralem  28182  1to2vfriswmgra  28184  1to3vfriswmgra  28185  a9e2ndeq  28325  en3lpVD  28621  undif3VD  28658  a9e2ndeqVD  28685  a9e2ndeqALT  28708  bnj964  28975  elpadd0  29998
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 177  df-or 359
  Copyright terms: Public domain W3C validator