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  2089  mooran1  2293  2eu3  2321  eueq3  3053  sbcor  3149  sspss  3390  sspsstr  3396  elun  3432  ssun  3470  inss  3514  undif3  3546  ifbi  3700  elpr2  3777  tpprceq3  3882  tppreqb  3883  pwpw0  3890  sssn  3901  snsssn  3910  preq12b  3917  prnebg  3922  pwsnALT  3953  unissint  4017  zfpair  4343  ordelinel  4621  ordssun  4622  ordequn  4623  onun2i  4638  unizlim  4639  reusv6OLD  4675  reusv7OLD  4676  ordeleqon  4710  ordunisuc  4753  orduninsuc  4764  tfinds  4780  limomss  4791  limom  4801  onxpdisj  4898  sotri2  5204  sotri3  5205  somincom  5212  funtpg  5442  bropopvvv  6366  soxp  6396  sorpssuni  6468  sorpssint  6469  tfr2b  6594  omopthi  6837  domnsym  7170  brwdom  7469  cantnfvalf  7554  iscard3  7908  cflim2  8077  sornom  8091  isfin5  8113  isfin6  8114  sdom2en01  8116  fin23lem29  8155  fin23lem30  8156  fin56  8207  fin67  8209  hsmexlem9  8239  axcc4dom  8255  axdc3lem2  8265  axdc3lem4  8267  brdom3  8340  winainflem  8502  r1tskina  8591  indpi  8718  renfdisj  9072  ltxrlt  9080  ltlen  9109  elnnnn0b  10197  nn0sub  10203  nn0n0n1ge2b  10214  elnn0z  10227  nn0ind-raph  10303  uzin  10451  indstr2  10487  xrnemnf  10651  xrnepnf  10652  mnfltxr  10657  nn0pnfge0  10661  xmullem2  10777  rexmul  10783  elfznelfzo  11120  injresinjlem  11127  injresinj  11128  m1expcl2  11331  sq01  11429  nn0opthi  11491  facp1  11499  faclbnd3  11511  faclbnd4lem1  11512  faclbnd4lem3  11514  bcn1  11532  hashnemnf  11556  hashv01gt1  11557  hashrabrsn  11576  hashunx  11588  sumz  12444  arisum  12567  arisum2  12568  divalglem1  12842  divalglem6  12846  gcdaddmlem  12956  mulgcd  12974  dfphi2  13091  4sqlem19  13259  ramz  13321  firest  13588  xpsfeq  13717  xpsfrnel2  13718  funcres2c  14026  sralem  16177  prmirred  16699  frgpcyg  16778  indiscld  17079  pnfnei  17207  mnfnei  17208  alexsubALTlem2  18001  alexsubALTlem3  18002  dscmet  18492  xrtgioo  18709  ishl2  19192  iunmbl2  19319  icombl  19326  ioombl  19327  recnprss  19659  recnperf  19660  dvexp2  19708  dvexp3  19730  dvne0f1  19764  plypf1  19999  taylfvallem1  20141  taylfval  20143  tayl0  20146  coseq0negpitopi  20279  logfac  20363  cxpexp  20427  pythag  20527  reasinsin  20604  harmonicbnd3  20714  lgslem4  20951  lgsquadlem2  21007  usgraedgprv  21264  usgraedgrnv  21265  usgraedg4  21273  usgraidx2v  21279  usgraexmpl  21287  nb3graprlem1  21327  wlkdvspthlem  21456  constr3trllem2  21487  vdgrf  21518  konigsberg  21558  ex-pr  21587  shunssi  22719  cvmdi  23676  iundisj2cnt  23994  xrge0iifiso  24126  esumpr2  24255  measiuns  24366  sxbrsigalem0  24416  subfacval3  24655  kur14lem7  24678  m1expevenALT  24685  nepss  24955  fz0n  24982  ntrivcvg  25005  prod1  25050  fprodfac  25076  dfon2lem7  25170  trpredlem1  25255  trpred0  25264  sltres  25343  altopthsn  25521  axlowdimlem15  25610  elhf2  25831  dissym1  25886  ordcmp  25912  itg2addnclem  25958  nn0prpw  26018  prtlem1  26382  hbtlem5  27002  m1expaddsub  27091  cnmsgnsubg  27104  ssrecnpr  27207  seff  27208  sblpnf  27209  expgrowthi  27220  dvconstbi  27221  19.33-2  27250  raaan2  27622  2reu3  27635  fvfundmfvn0  27657  afvpcfv0  27680  afvfv0bi  27686  afvco2  27710  3vfriswmgralem  27758  1to2vfriswmgra  27760  1to3vfriswmgra  27761  vdgfrgragt2  27782  frgrawopreglem2  27798  frgrawopreglem3  27799  frgraregorufr0  27805  a9e2ndeq  27990  en3lpVD  28299  undif3VD  28336  a9e2ndeqVD  28363  a9e2ndeqALT  28386  bnj964  28653  dfsb2NEW7  28972  elpadd0  29924
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