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

Theorem mpjaodan 784
Description: Eliminate a disjunction in a deduction. A translation of natural deduction rule  \/ E ( \/ elimination), see natded 24817. (Contributed by Mario Carneiro, 29-May-2016.)
Hypotheses
Ref Expression
jaodan.1  |-  ( (
ph  /\  ps )  ->  ch )
jaodan.2  |-  ( (
ph  /\  th )  ->  ch )
jaodan.3  |-  ( ph  ->  ( ps  \/  th ) )
Assertion
Ref Expression
mpjaodan  |-  ( ph  ->  ch )

Proof of Theorem mpjaodan
StepHypRef Expression
1 jaodan.3 . 2  |-  ( ph  ->  ( ps  \/  th ) )
2 jaodan.1 . . 3  |-  ( (
ph  /\  ps )  ->  ch )
3 jaodan.2 . . 3  |-  ( (
ph  /\  th )  ->  ch )
42, 3jaodan 783 . 2  |-  ( (
ph  /\  ( ps  \/  th ) )  ->  ch )
51, 4mpdan 668 1  |-  ( ph  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ wo 368    /\ wa 369
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 185  df-or 370  df-an 371
This theorem is referenced by:  mpjao3dan  1295  weniso  6237  isf32lem2  8733  isf32lem4  8735  fpwwe2lem11  9017  fpwwe2lem12  9018  lecasei  9689  ltlecasei  9691  xaddass  11440  xlesubadd  11454  xmulge0  11475  xadddi2  11488  xrsupss  11499  xrinfmss  11500  seqf1olem2  12114  expaddzlem  12176  discr  12270  fzomaxdif  13138  iseralt  13469  sumrb  13497  telfsumo  13578  fsumparts  13582  bitsf1  13954  smupvallem  13991  eucalgf  14070  eucalginv  14071  vdwmc2  14355  mreexmrid  14897  mreexexlem3d  14900  mulgnn0p1  15960  mulgnn0subcl  15962  mulgsubcl  15963  mulgneg  15967  mulgz  15970  mulgnn0dir  15972  mulgdirlem  15973  mulgdir  15974  submmulg  15984  ghmmulg  16081  odid  16365  oddvds  16374  dfod2  16389  gexid  16404  gexdvds  16407  mulgnn0di  16637  mulgdi  16638  gsumzsplit  16744  gsumzsplitOLD  16745  lsppratlem5  17592  prmirred  18308  prmirredOLD  18311  1stckgenlem  19805  qtoprest  19969  tgpmulg  20343  tsmssplit  20405  xblss2ps  20655  xblss2  20656  metustfbasOLD  20819  metustfbas  20820  nmoix  20987  nmoleub  20989  idnghm  21001  blcvx  21054  icccmp  21081  xrge0tsms  21090  metdstri  21106  nmoleub2lem  21348  rrxcph  21575  rrxdstprj1  21587  ivthle  21619  ivthle2  21620  dyadmbl  21760  volivth  21767  itg2const2  21899  itg2mulc  21905  dvlip2  22147  dvfsumlem1  22178  mdegmullem  22229  coemulhi  22401  dgrcolem2  22421  coseq00topi  22644  abssinper  22660  cxplea  22821  cxple2  22822  cxple2a  22824  cxpcn3  22866  cxpaddlelem  22869  cxpaddle  22870  ang180lem3  22887  dcubic2  22919  birthdaylem2  23026  jensen  23062  ppiltx  23195  chtub  23231  bcmono  23296  bcmax  23297  bpos  23312  lgseisenlem1  23368  2sqlem4  23386  pntrlog2bndlem5  23510  pntpbnd1  23515  tgcgrextend  23620  tgbtwnexch2  23631  tgldimor  23637  tgifscgr  23644  tgcgrxfr  23653  tgbtwnconn1  23705  tgbtwnconn2  23706  tgbtwnconn3  23707  tgbtwnconnln3  23708  tgbtwnconn22  23709  tgbtwnconnln1  23710  tgbtwnconnln2  23711  legtrid  23721  legbtwn  23724  legov3  23727  ncolncol  23755  krippen  23792  midexlem  23793  mideu  23830  ex-natded5.7  24825  ex-natded5.13  24829  ex-natded9.20  24831  ex-natded9.20-2  24832  xrge0infss  27264  difioo  27277  iundisjcnt  27287  xrsmulgzz  27344  ressmulgnn0  27350  xrge0addgt0  27359  xrge0adddir  27360  archirngz  27411  archiabllem2a  27416  xrge0tsmsd  27454  xrge0mulc1cn  27575  qqhval2lem  27614  nexple  27661  esumpcvgval  27740  esumcvg  27748  sigaclcu3  27778  measiuns  27844  voliune  27857  volfiniune  27858  volmeas  27859  sgncl  28133  sgnmul  28137  gsumnunsn  28149  signsply0  28164  signswch  28174  signslema  28175  signstfvneq0  28185  ntrivcvgtail  28627  prodrb  28657  fdc  29857  orel  30123  pell1qrgaplem  30429  monotoddzzfi  30498  oddcomabszz  30500  zindbi  30502  rmxnn  30509  jm2.24  30521  acongeq  30541  jm2.23  30558  jm2.26lem3  30563  wepwsolem  30607  fnchoice  30998  refsum2cnlem1  31006  wallispilem3  31383  bnj517  33031  bnj1408  33180  bnj1423  33195  bnj1452  33196  lsatcvat  33856  lkrpssN  33969  2at0mat0  34330  atmod1i1m  34663  lhp2at0nle  34840  trlcone  35533  tendoex  35780  dihlspsnssN  36138  dochkrsm  36264  lcfl8  36308  lclkrlem2b  36314  lclkrlem2s  36331  lcfrlem21  36369  mapdval2N  36436  mapdspex  36474
  Copyright terms: Public domain W3C validator