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

Theorem mpjaodan 761
Description: Eliminate a disjunction in a deduction. A translation of natural deduction rule  \/ E ( \/ elimination), see natded 20790. (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 760 . 2  |-  ( (
ph  /\  ( ps  \/  th ) )  ->  ch )
51, 4mpdan 649 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 357    /\ wa 358
This theorem is referenced by:  weniso  5852  isf32lem2  7980  isf32lem4  7982  fpwwe2lem11  8262  fpwwe2lem12  8263  lecasei  8926  ltlecasei  8928  xaddass  10569  xlesubadd  10583  xmulge0  10604  xadddi2  10617  xrsupss  10627  xrinfmss  10628  seqf1olem2  11086  expaddzlem  11145  discr  11238  fzomaxdif  11827  iseralt  12157  sumrb  12186  fsumtscopo  12260  fsumparts  12264  bitsf1  12637  smupvallem  12674  eucalgf  12753  eucalginv  12754  vdwmc2  13026  mreexmrid  13545  mreexexlem3d  13548  mulgnn0p1  14578  mulgnn0subcl  14580  mulgsubcl  14581  mulgneg  14585  mulgz  14588  mulgnn0dir  14590  mulgdirlem  14591  mulgdir  14592  submmulg  14602  ghmmulg  14695  odid  14853  oddvds  14862  dfod2  14877  gexid  14892  gexdvds  14895  mulgnn0di  15125  mulgdi  15126  gsumzsplit  15206  lsppratlem5  15904  prmirred  16448  1stckgenlem  17248  qtoprest  17408  tgpmulg  17776  tsmssplit  17834  xblss2  17958  nmoix  18238  nmoleub  18240  idnghm  18252  blcvx  18304  icccmp  18330  xrge0tsms  18339  metdstri  18355  nmoleub2lem  18595  ivthle  18816  ivthle2  18817  dyadmbl  18955  volivth  18962  itg2const2  19096  itg2mulc  19102  dvlip2  19342  dvfsumlem1  19373  mdegmullem  19464  coemulhi  19635  dgrcolem2  19655  coseq00topi  19870  abssinper  19886  cxplea  20043  cxple2  20044  cxple2a  20046  cxpcn3  20088  cxpaddlelem  20091  cxpaddle  20092  ang180lem3  20109  dcubic2  20140  birthdaylem2  20247  jensen  20283  ppiltx  20415  chtub  20451  bcmono  20516  bcmax  20517  bpos  20532  lgseisenlem1  20588  2sqlem4  20606  pntrlog2bndlem5  20730  pntpbnd1  20735  ex-natded5.7  20798  ex-natded5.13  20802  ex-natded9.20  20804  ex-natded9.20-2  20805  elpreq  23188  difioo  23275  ssnnssfz  23277  xrsmulgzz  23307  ressmulgnn0  23309  xrge0mulc1cn  23323  xrge0addgt0  23331  xrge0adddir  23332  iundisjcnt  23367  xrge0tsmsd  23382  hashge1  23388  nnlogbexp  23406  esumcst  23436  esumpcvgval  23446  esumcvg  23454  sigaclcu3  23483  fdc  26455  pell1qrgaplem  26958  monotoddzzfi  27027  oddcomabszz  27029  zindbi  27031  rmxnn  27038  jm2.24  27050  acongeq  27070  jm2.23  27089  jm2.26lem3  27094  wepwsolem  27138  fnchoice  27700  refsum2cnlem1  27708  bnj517  28917  bnj1408  29066  bnj1423  29081  bnj1452  29082  lsatcvat  29240  lkrpssN  29353  2at0mat0  29714  atmod1i1m  30047  lhp2at0nle  30224  trlcone  30917  tendoex  31164  dihlspsnssN  31522  dochkrsm  31648  lcfl8  31692  lclkrlem2b  31698  lclkrlem2s  31715  lcfrlem21  31753  mapdval2N  31820  mapdspex  31858
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360
  Copyright terms: Public domain W3C validator