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 23610. (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  1285  weniso  6045  isf32lem2  8523  isf32lem4  8525  fpwwe2lem11  8807  fpwwe2lem12  8808  lecasei  9480  ltlecasei  9482  xaddass  11212  xlesubadd  11226  xmulge0  11247  xadddi2  11260  xrsupss  11271  xrinfmss  11272  seqf1olem2  11846  expaddzlem  11907  discr  12001  fzomaxdif  12831  iseralt  13162  sumrb  13190  fsumtscopo  13265  fsumparts  13269  bitsf1  13642  smupvallem  13679  eucalgf  13758  eucalginv  13759  vdwmc2  14040  mreexmrid  14581  mreexexlem3d  14584  mulgnn0p1  15638  mulgnn0subcl  15640  mulgsubcl  15641  mulgneg  15645  mulgz  15648  mulgnn0dir  15650  mulgdirlem  15651  mulgdir  15652  submmulg  15662  ghmmulg  15759  odid  16041  oddvds  16050  dfod2  16065  gexid  16080  gexdvds  16083  mulgnn0di  16313  mulgdi  16314  gsumzsplit  16418  gsumzsplitOLD  16419  lsppratlem5  17232  prmirred  17919  prmirredOLD  17922  1stckgenlem  19126  qtoprest  19290  tgpmulg  19664  tsmssplit  19726  xblss2ps  19976  xblss2  19977  metustfbasOLD  20140  metustfbas  20141  nmoix  20308  nmoleub  20310  idnghm  20322  blcvx  20375  icccmp  20402  xrge0tsms  20411  metdstri  20427  nmoleub2lem  20669  rrxcph  20896  rrxdstprj1  20908  ivthle  20940  ivthle2  20941  dyadmbl  21080  volivth  21087  itg2const2  21219  itg2mulc  21225  dvlip2  21467  dvfsumlem1  21498  mdegmullem  21549  coemulhi  21721  dgrcolem2  21741  coseq00topi  21964  abssinper  21980  cxplea  22141  cxple2  22142  cxple2a  22144  cxpcn3  22186  cxpaddlelem  22189  cxpaddle  22190  ang180lem3  22207  dcubic2  22239  birthdaylem2  22346  jensen  22382  ppiltx  22515  chtub  22551  bcmono  22616  bcmax  22617  bpos  22632  lgseisenlem1  22688  2sqlem4  22706  pntrlog2bndlem5  22830  pntpbnd1  22835  tgcgrextend  22939  tgbtwnexch2  22949  tgldimor  22955  tgifscgr  22961  tgcgrxfr  22970  tgbtwnconn1  23007  tgbtwnconn2  23008  tgbtwnconn3  23009  tgbtwnconnln3  23010  tgbtwnconnln1  23011  tgbtwnconnln2  23012  legtrid  23022  legbtwn  23025  ncolncol  23051  krippen  23085  midexlem  23086  ex-natded5.7  23618  ex-natded5.13  23622  ex-natded9.20  23624  ex-natded9.20-2  23625  xrge0infss  26053  difioo  26072  iundisjcnt  26082  xrsmulgzz  26139  ressmulgnn0  26145  xrge0addgt0  26154  xrge0adddir  26155  archirngz  26206  archiabllem2a  26211  xrge0tsmsd  26253  xrge0mulc1cn  26371  qqhval2lem  26410  nexple  26448  esumpcvgval  26527  esumcvg  26535  sigaclcu3  26565  measiuns  26631  voliune  26645  volfiniune  26646  volmeas  26647  sgncl  26921  sgnmul  26925  gsumnunsn  26937  signsply0  26952  signswch  26962  signslema  26963  signsvtn0  26971  signstfvneq0  26973  ntrivcvgtail  27415  prodrb  27445  fdc  28641  orel  28907  pell1qrgaplem  29214  monotoddzzfi  29283  oddcomabszz  29285  zindbi  29287  rmxnn  29294  jm2.24  29306  acongeq  29326  jm2.23  29345  jm2.26lem3  29350  wepwsolem  29394  fnchoice  29751  refsum2cnlem1  29759  wallispilem3  29862  bnj517  31878  bnj1408  32027  bnj1423  32042  bnj1452  32043  lsatcvat  32695  lkrpssN  32808  2at0mat0  33169  atmod1i1m  33502  lhp2at0nle  33679  trlcone  34372  tendoex  34619  dihlspsnssN  34977  dochkrsm  35103  lcfl8  35147  lclkrlem2b  35153  lclkrlem2s  35170  lcfrlem21  35208  mapdval2N  35275  mapdspex  35313
  Copyright terms: Public domain W3C validator