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

Theorem mpjaodan 763
Description: Eliminate a disjunction in a deduction. A translation of natural deduction rule  \/ E ( \/ elimination), see natded 4. (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 762 . 2  |-  ( (
ph  /\  ( ps  \/  th ) )  ->  ch )
51, 4mpdan 651 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 6    \/ wo 359    /\ wa 360
This theorem is referenced by:  weniso  5814  isf32lem2  7976  isf32lem4  7978  fpwwe2lem11  8258  fpwwe2lem12  8259  lecasei  8922  ltlecasei  8924  xaddass  10564  xlesubadd  10578  xmulge0  10599  xadddi2  10612  xrsupss  10622  xrinfmss  10623  seqf1olem2  11081  expaddzlem  11140  discr  11233  fzomaxdif  11822  iseralt  12152  sumrb  12181  fsumtscopo  12255  fsumparts  12259  bitsf1  12632  smupvallem  12669  eucalgf  12748  eucalginv  12749  vdwmc2  13021  mreexmrid  13540  mreexexlem3d  13543  mulgnn0p1  14573  mulgnn0subcl  14575  mulgsubcl  14576  mulgneg  14580  mulgz  14583  mulgnn0dir  14585  mulgdirlem  14586  mulgdir  14587  submmulg  14597  ghmmulg  14690  odid  14848  oddvds  14857  dfod2  14872  gexid  14887  gexdvds  14890  mulgnn0di  15120  mulgdi  15121  gsumzsplit  15201  lsppratlem5  15899  prmirred  16443  1stckgenlem  17243  qtoprest  17403  tgpmulg  17771  tsmssplit  17829  xblss2  17953  nmoix  18233  nmoleub  18235  idnghm  18247  blcvx  18299  icccmp  18325  xrge0tsms  18334  metdstri  18350  nmoleub2lem  18590  ivthle  18811  ivthle2  18812  dyadmbl  18950  volivth  18957  itg2const2  19091  itg2mulc  19097  dvlip2  19337  dvfsumlem1  19368  mdegmullem  19459  coemulhi  19630  dgrcolem2  19650  coseq00topi  19865  abssinper  19881  cxplea  20038  cxple2  20039  cxple2a  20041  cxpcn3  20083  cxpaddlelem  20086  cxpaddle  20087  ang180lem3  20104  dcubic2  20135  birthdaylem2  20242  jensen  20278  ppiltx  20410  chtub  20446  bcmono  20511  bcmax  20512  bpos  20527  lgseisenlem1  20583  2sqlem4  20601  pntrlog2bndlem5  20725  pntpbnd1  20730  ex-natded5.7  20819  ex-natded5.13  20823  ex-natded9.20  20825  ex-natded9.20-2  20826  fdc  25855  pell1qrgaplem  26358  monotoddzzfi  26427  oddcomabszz  26429  zindbi  26431  rmxnn  26438  jm2.24  26450  acongeq  26470  jm2.23  26489  jm2.26lem3  26494  wepwsolem  26538  fnchoice  27100  refsum2cnlem1  27108  bnj517  28185  bnj1408  28334  bnj1423  28349  bnj1452  28350  lsatcvat  28508  lkrpssN  28621  2at0mat0  28982  atmod1i1m  29315  lhp2at0nle  29492  trlcone  30185  tendoex  30432  dihlspsnssN  30790  dochkrsm  30916  lcfl8  30960  lclkrlem2b  30966  lclkrlem2s  30983  lcfrlem21  31021  mapdval2N  31088  mapdspex  31126
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362
  Copyright terms: Public domain W3C validator