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

Theorem jaoi 370
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 364 . . 3  |-  ( (
ph  \/  ch )  ->  ( -.  ph  ->  ch ) )
2 jaoi.2 . . 3  |-  ( ch 
->  ps )
31, 2syl6 32 . 2  |-  ( (
ph  \/  ch )  ->  ( -.  ph  ->  ps ) )
4 jaoi.1 . 2  |-  ( ph  ->  ps )
53, 4pm2.61d2 155 1  |-  ( (
ph  \/  ch )  ->  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 359
This theorem is referenced by:  jaod  371  pm1.4  377  jaoa  498  pm1.2  501  orim12i  504  pm1.5  510  pm2.41  558  pm2.42  559  pm2.4  560  pm4.44  562  jaoian  761  pm2.64  766  pm2.82  827  pm3.2ni  829  andi  839  ecase3  909  consensus  927  cad1  1408  19.33  1618  19.33b  1619  dfsb2  2110  mooran1  2337  2eu3  2365  eueq3  3111  sbcor  3207  sspss  3448  sspsstr  3454  elun  3490  ssun  3528  inss  3572  undif3  3604  ifbi  3758  elpr2  3835  tpprceq3  3940  tppreqb  3941  pwpw0  3948  sssn  3959  snsssn  3969  preq12b  3976  prnebg  3981  pwsnALT  4012  unissint  4076  zfpair  4404  ordelinel  4683  ordssun  4684  ordequn  4685  onun2i  4700  unizlim  4701  reusv6OLD  4737  reusv7OLD  4738  ordeleqon  4772  ordunisuc  4815  orduninsuc  4826  tfinds  4842  limomss  4853  limom  4863  onxpdisj  4960  sotri2  5266  sotri3  5267  somincom  5274  funtpg  5504  fvfundmfvn0  5765  bropopvvv  6429  soxp  6462  sorpssuni  6534  sorpssint  6535  tfr2b  6660  omopthi  6903  domnsym  7236  brwdom  7538  cantnfvalf  7623  iscard3  7979  cflim2  8148  sornom  8162  isfin5  8184  isfin6  8185  sdom2en01  8187  fin23lem29  8226  fin23lem30  8227  fin56  8278  fin67  8280  hsmexlem9  8310  axcc4dom  8326  axdc3lem2  8336  axdc3lem4  8338  brdom3  8411  winainflem  8573  r1tskina  8662  indpi  8789  renfdisj  9143  ltxrlt  9151  ltlen  9180  elnnnn0b  10269  nn0sub  10275  nn0n0n1ge2b  10286  elnn0z  10299  nn0ind-raph  10375  uzin  10523  indstr2  10559  xrnemnf  10723  xrnepnf  10724  mnfltxr  10729  nn0pnfge0  10733  xmullem2  10849  rexmul  10855  elfznelfzo  11197  injresinjlem  11204  injresinj  11205  m1expcl2  11408  sq01  11506  nn0opthi  11568  facp1  11576  faclbnd3  11588  faclbnd4lem1  11589  faclbnd4lem3  11591  bcn1  11609  hashnemnf  11633  hashv01gt1  11634  hashrabrsn  11653  hashunx  11665  sumz  12521  arisum  12644  arisum2  12645  divalglem1  12919  divalglem6  12923  gcdaddmlem  13033  mulgcd  13051  dfphi2  13168  4sqlem19  13336  ramz  13398  firest  13665  xpsfeq  13794  xpsfrnel2  13795  funcres2c  14103  sralem  16254  prmirred  16780  frgpcyg  16859  indiscld  17160  pnfnei  17289  mnfnei  17290  alexsubALTlem2  18084  alexsubALTlem3  18085  dscmet  18625  xrtgioo  18842  ishl2  19329  iunmbl2  19456  icombl  19463  ioombl  19464  recnprss  19796  recnperf  19797  dvexp2  19845  dvexp3  19867  dvne0f1  19901  plypf1  20136  taylfvallem1  20278  taylfval  20280  tayl0  20283  coseq0negpitopi  20416  logfac  20500  cxpexp  20564  pythag  20664  reasinsin  20741  harmonicbnd3  20851  lgslem4  21088  lgsquadlem2  21144  usgraedgprv  21401  usgraedgrnv  21402  usgraedg4  21411  usgraidx2v  21417  usgraexmpl  21425  nb3graprlem1  21465  wlkdvspthlem  21612  constr3trllem2  21643  vdgrf  21674  konigsberg  21714  ex-pr  21743  shunssi  22875  cvmdi  23832  iundisj2cnt  24160  xrge0iifiso  24326  esumpr2  24463  measiuns  24576  sxbrsigalem0  24626  subfacval3  24880  kur14lem7  24903  m1expevenALT  24910  nepss  25180  fz0n  25207  ntrivcvg  25230  prod1  25275  fprodfac  25301  dfon2lem7  25421  trpredlem1  25510  trpred0  25519  sltres  25624  altopthsn  25811  axlowdimlem15  25900  elhf2  26121  dissym1  26176  ordcmp  26202  tan2h  26252  itg2addnclem  26270  nn0prpw  26340  prtlem1  26704  hbtlem5  27323  m1expaddsub  27412  cnmsgnsubg  27425  ssrecnpr  27528  seff  27529  sblpnf  27530  expgrowthi  27541  dvconstbi  27542  19.33-2  27571  raaan2  27943  2reu3  27956  afvpcfv0  28000  afvfv0bi  28006  afvco2  28030  jaoi3  28062  elovmpt3rab1  28107  swrdnd  28216  swrdvalodm2  28222  swrdvalodm  28223  usgra2wlkspthlem1  28344  usgra2adedgspthlem2  28352  2wlkonot3v  28407  2spthonot3v  28408  3vfriswmgralem  28468  1to2vfriswmgra  28470  1to3vfriswmgra  28471  vdgfrgragt2  28492  frgrawopreglem2  28508  frgrawopreglem3  28509  frgraregorufr0  28515  a9e2ndeq  28720  en3lpVD  29031  undif3VD  29068  a9e2ndeqVD  29095  a9e2ndeqALT  29117  bnj964  29388  dfsb2NEW7  29712  elpadd0  30680
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 179  df-or 361
  Copyright terms: Public domain W3C validator