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  1597  19.33b  1598  dfsb2  2008  mooran1  2210  2eu3  2238  eueq3  2953  sbcor  3048  sspss  3288  sspsstr  3294  elun  3329  ssun  3367  inss  3411  undif3  3442  ifbi  3595  elpr2  3672  pwpw0  3779  sssn  3788  snsssn  3797  preq12b  3804  pwsnALT  3838  unissint  3902  zfpair  4228  pwundifOLD  4317  ordelinel  4507  ordssun  4508  ordequn  4509  onun2i  4524  unizlim  4525  reusv6OLD  4561  reusv7OLD  4562  ordeleqon  4596  ordunisuc  4639  orduninsuc  4650  tfinds  4666  limomss  4677  limom  4687  onxpdisj  4785  sotri2  5088  sotri3  5089  somincom  5096  soxp  6244  sorpssuni  6302  sorpssint  6303  tfr2b  6428  omopthi  6671  domnsym  7003  brwdom  7297  cantnfvalf  7382  iscard3  7736  cflim2  7905  sornom  7919  isfin5  7941  isfin6  7942  sdom2en01  7944  fin23lem29  7983  fin23lem30  7984  fin56  8035  fin67  8037  hsmexlem9  8067  axcc4dom  8083  axdc3lem2  8093  axdc3lem4  8095  brdom3  8169  winainflem  8331  r1tskina  8420  indpi  8547  renfdisj  8901  ltxrlt  8909  ltlen  8938  elnnnn0b  10024  nn0sub  10030  elnn0z  10052  nn0ind-raph  10128  uzin  10276  indstr2  10312  xrnemnf  10476  xrnepnf  10477  mnfltxr  10482  xmullem2  10601  rexmul  10607  m1expcl2  11141  sq01  11239  nn0opthi  11301  facp1  11309  faclbnd3  11321  faclbnd4lem1  11322  faclbnd4lem3  11324  bcn1  11341  sumz  12211  arisum  12334  arisum2  12335  divalglem1  12609  divalglem6  12613  gcdaddmlem  12723  mulgcd  12741  dfphi2  12858  4sqlem19  13026  ramz  13088  firest  13353  xpsfeq  13482  xpsfrnel2  13483  funcres2c  13791  sralem  15946  prmirred  16464  frgpcyg  16543  indiscld  16844  pnfnei  16966  mnfnei  16967  alexsubALTlem2  17758  alexsubALTlem3  17759  dscmet  18111  xrtgioo  18328  ishl2  18803  iunmbl2  18930  icombl  18937  ioombl  18938  recnprss  19270  recnperf  19271  dvexp2  19319  dvexp3  19341  dvne0f1  19375  plypf1  19610  taylfvallem1  19752  taylfval  19754  tayl0  19757  coseq0negpitopi  19887  logfac  19970  cxpexp  20031  pythag  20131  reasinsin  20208  harmonicbnd3  20317  lgslem4  20554  lgsquadlem2  20610  ex-pr  20833  shunssi  21963  cvmdi  22920  xrge0iifiso  23332  iundisj2cnt  23383  esumpr2  23454  measiuns  23559  subfacval3  23735  kur14lem7  23758  konigsberg  23926  nepss  24087  fz0n  24112  prod1  24169  dfon2lem7  24216  trpredlem1  24301  trpred0  24310  sltres  24389  altopthsn  24567  axlowdimlem15  24656  elhf2  24877  dissym1  24932  ordcmp  24958  itg2addnclem  25003  facrm  25056  nxtor  25088  untindd  25122  neiopne  25154  cbcpcp  25265  tolat  25389  basexre  25625  cntrset  25705  intvconlem1  25806  vtarsuelt  25998  inttarcar  26004  fnckle  26148  pfsubkl  26150  pdiveql  26271  nn0prpw  26342  prtlem1  26810  hbtlem5  27435  m1expaddsub  27524  cnmsgnsubg  27537  ssrecnpr  27640  seff  27641  sblpnf  27642  expgrowthi  27653  dvconstbi  27654  19.33-2  27683  raaan2  28056  2reu3  28069  fvfundmfvn0  28091  afvpcfv0  28114  afvfv0bi  28120  afvco2  28144  tpprceq3  28182  elfznelfzo  28213  injresinjlem  28214  injresinj  28215  usgraedgprv  28256  usgraedgrnv  28257  usgraexmpl  28267  nb3graprlem1  28287  trlonprop  28341  wlkdvspthlem  28365  constr3trllem2  28397  3vfriswmgralem  28428  1to2vfriswmgra  28430  1to3vfriswmgra  28431  a9e2ndeq  28624  en3lpVD  28937  undif3VD  28974  a9e2ndeqVD  29001  a9e2ndeqALT  29024  bnj964  29291  dfsb2NEW7  29609  elpadd0  30620
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