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

Theorem mpjaodan 794
Description: Eliminate a disjunction in a deduction. A translation of natural deduction rule  \/ E ( \/ elimination), see natded 25846. (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 793 . 2  |-  ( (
ph  /\  ( ps  \/  th ) )  ->  ch )
51, 4mpdan 673 1  |-  ( ph  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ wo 370    /\ wa 371
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 189  df-or 372  df-an 373
This theorem is referenced by:  mpjao3dan  1334  weniso  6243  isf32lem2  8781  isf32lem4  8783  fpwwe2lem11  9062  fpwwe2lem12  9063  lecasei  9737  ltlecasei  9739  xaddass  11532  xlesubadd  11546  xmulge0  11567  xadddi2  11580  xrsupss  11591  xrinfmss  11592  fzm1  11871  seqf1olem2  12250  expaddzlem  12312  discr  12406  fzomaxdif  13399  iseralt  13744  sumrb  13772  telfsumo  13855  fsumparts  13859  ntrivcvgtail  13949  prodrb  13979  bitsf1  14413  smupvallem  14450  eucalgf  14535  eucalginv  14536  vdwmc2  14922  mreexmrid  15542  mreexexlem3d  15545  mulgnn0p1  16762  mulgnn0subcl  16764  mulgsubcl  16765  mulgneg  16769  mulgz  16772  mulgnn0dir  16774  mulgdirlem  16775  mulgdir  16776  submmulg  16786  ghmmulg  16888  odid  17180  oddvds  17189  odidOLD  17196  dfod2  17208  gexid  17225  gexdvds  17228  mulgnn0di  17459  mulgdi  17460  gsumzsplit  17553  lsppratlem5  18367  prmirred  19059  1stckgenlem  20561  qtoprest  20725  tgpmulg  21101  tsmssplit  21159  xblss2ps  21409  xblss2  21410  metustfbas  21565  nmoix  21727  nmoleub  21729  nmoixOLD  21743  nmoleubOLD  21745  idnghm  21757  blcvx  21809  icccmp  21836  xrge0tsms  21845  metdstri  21861  metdstriOLD  21876  nmoleub2lem  22121  rrxcph  22344  rrxdstprj1  22356  ivthle  22400  ivthle2  22401  dyadmbl  22551  volivth  22558  itg2const2  22692  itg2mulc  22698  dvlip2  22940  dvfsumlem1  22971  mdegmullem  23020  coemulhi  23201  dgrcolem2  23221  coseq00topi  23450  abssinper  23466  cxplea  23634  cxple2  23635  cxple2a  23637  cxpcn3  23681  cxpaddlelem  23684  cxpaddle  23685  ang180lem3  23733  dcubic2  23763  birthdaylem2  23871  jensen  23907  ppiltx  24097  chtub  24133  bcmono  24198  bcmax  24199  bpos  24214  lgseisenlem1  24270  2sqlem4  24288  pntrlog2bndlem5  24412  pntpbnd1  24417  tgldimor  24539  tgifscgr  24546  tgcgrxfr  24556  tgbtwnconn1  24613  tgbtwnconn2  24614  tgbtwnconn3  24615  tgbtwnconnln3  24616  tgbtwnconn22  24617  tgbtwnconnln1  24618  tgbtwnconnln2  24619  legtrid  24629  legbtwn  24632  tgcgrsub2  24633  legov3  24636  hlln  24645  hltr  24648  btwnhl  24652  ncolncol  24684  mirconn  24716  krippen  24729  midexlem  24730  midex  24772  opphllem2  24783  opphllem5  24786  opphllem6  24787  outpasch  24790  hlpasch  24791  trgcopyeulem  24840  cgrahl  24861  cgracol  24862  ex-natded5.7  25854  ex-natded5.13  25858  ex-natded9.20  25860  ex-natded9.20-2  25861  xrge0infss  28333  xrge0infssOLD  28334  difioo  28357  iundisjcnt  28367  f1ocnt  28369  2sqmod  28402  xrsmulgzz  28433  ressmulgnn0  28439  xrge0addgt0  28447  xrge0adddir  28448  archirngz  28499  archiabllem2a  28504  xrge0tsmsd  28541  submateq  28628  lmat22lem  28636  locfinref  28661  xrge0mulc1cn  28740  qqhval2lem  28778  nexple  28824  esumpcvgval  28892  esumcvg  28900  sigaclcu3  28937  measiuns  29032  voliune  29045  volfiniune  29046  volmeas  29047  sgncl  29402  sgnmul  29406  gsumnunsn  29418  signsply0  29433  signswch  29443  signslema  29444  signstfvneq0  29454  bnj517  29689  bnj1408  29838  bnj1423  29853  bnj1452  29854  poimirlem2  31935  fdc  32067  orel  32332  lsatcvat  32610  lkrpssN  32723  2at0mat0  33084  atmod1i1m  33417  lhp2at0nle  33594  trlcone  34289  tendoex  34536  dihlspsnssN  34894  dochkrsm  35020  lcfl8  35064  lclkrlem2b  35070  lclkrlem2s  35087  lcfrlem21  35125  mapdval2N  35192  mapdspex  35230  pell1qrgaplem  35713  monotoddzzfi  35784  oddcomabszz  35786  zindbi  35788  rmxnn  35795  jm2.24  35807  acongeq  35827  jm2.23  35845  jm2.26lem3  35850  wepwsolem  35894  frege102d  36340  fnchoice  37344  refsum2cnlem1  37352  wallispilem3  37923  wtgoldbnnsum4prm  38891  bgoldbnnsum3prm  38893  nn0sumshdiglem1  40419
  Copyright terms: Public domain W3C validator