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

Theorem mpjaodan 793
Description: Eliminate a disjunction in a deduction. A translation of natural deduction rule  \/ E ( \/ elimination), see natded 25739. (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 792 . 2  |-  ( (
ph  /\  ( ps  \/  th ) )  ->  ch )
51, 4mpdan 672 1  |-  ( ph  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ wo 369    /\ wa 370
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 188  df-or 371  df-an 372
This theorem is referenced by:  mpjao3dan  1331  weniso  6251  isf32lem2  8773  isf32lem4  8775  fpwwe2lem11  9054  fpwwe2lem12  9055  lecasei  9729  ltlecasei  9731  xaddass  11524  xlesubadd  11538  xmulge0  11559  xadddi2  11572  xrsupss  11583  xrinfmss  11584  fzm1  11861  seqf1olem2  12239  expaddzlem  12301  discr  12395  fzomaxdif  13374  iseralt  13718  sumrb  13746  telfsumo  13829  fsumparts  13833  ntrivcvgtail  13923  prodrb  13953  bitsf1  14383  smupvallem  14420  eucalgf  14502  eucalginv  14503  vdwmc2  14889  mreexmrid  15501  mreexexlem3d  15504  mulgnn0p1  16721  mulgnn0subcl  16723  mulgsubcl  16724  mulgneg  16728  mulgz  16731  mulgnn0dir  16733  mulgdirlem  16734  mulgdir  16735  submmulg  16745  ghmmulg  16847  odid  17132  oddvds  17141  dfod2  17156  gexid  17173  gexdvds  17176  mulgnn0di  17407  mulgdi  17408  gsumzsplit  17501  lsppratlem5  18315  prmirred  19003  1stckgenlem  20505  qtoprest  20669  tgpmulg  21045  tsmssplit  21103  xblss2ps  21353  xblss2  21354  metustfbas  21509  nmoix  21671  nmoleub  21673  nmoixOLD  21687  nmoleubOLD  21689  idnghm  21701  blcvx  21753  icccmp  21780  xrge0tsms  21789  metdstri  21805  nmoleub2lem  22047  rrxcph  22270  rrxdstprj1  22282  ivthle  22314  ivthle2  22315  dyadmbl  22465  volivth  22472  itg2const2  22606  itg2mulc  22612  dvlip2  22854  dvfsumlem1  22885  mdegmullem  22934  coemulhi  23115  dgrcolem2  23135  coseq00topi  23361  abssinper  23377  cxplea  23545  cxple2  23546  cxple2a  23548  cxpcn3  23592  cxpaddlelem  23595  cxpaddle  23596  ang180lem3  23644  dcubic2  23674  birthdaylem2  23782  jensen  23818  ppiltx  24006  chtub  24042  bcmono  24107  bcmax  24108  bpos  24123  lgseisenlem1  24179  2sqlem4  24197  pntrlog2bndlem5  24321  pntpbnd1  24326  tgldimor  24448  tgifscgr  24455  tgcgrxfr  24464  tgbtwnconn1  24519  tgbtwnconn2  24520  tgbtwnconn3  24521  tgbtwnconnln3  24522  tgbtwnconn22  24523  tgbtwnconnln1  24524  tgbtwnconnln2  24525  legtrid  24535  legbtwn  24538  tgcgrsub2  24539  legov3  24542  hlln  24551  hltr  24554  btwnhl  24558  ncolncol  24590  mirconn  24621  krippen  24632  midexlem  24633  midex  24675  opphllem2  24686  opphllem5  24689  opphllem6  24690  outpasch  24693  hlpasch  24694  trgcopyeulem  24743  cgrahl  24763  cgracol  24764  ex-natded5.7  25747  ex-natded5.13  25751  ex-natded9.20  25753  ex-natded9.20-2  25754  xrge0infss  28222  difioo  28241  iundisjcnt  28251  f1ocnt  28253  2sqmod  28288  xrsmulgzz  28318  ressmulgnn0  28324  xrge0addgt0  28333  xrge0adddir  28334  archirngz  28385  archiabllem2a  28390  xrge0tsmsd  28428  submateq  28515  lmat22lem  28523  locfinref  28548  xrge0mulc1cn  28627  qqhval2lem  28665  nexple  28711  esumpcvgval  28779  esumcvg  28787  sigaclcu3  28824  measiuns  28919  voliune  28932  volfiniune  28933  volmeas  28934  sgncl  29238  sgnmul  29242  gsumnunsn  29254  signsply0  29269  signswch  29279  signslema  29280  signstfvneq0  29290  bnj517  29525  bnj1408  29674  bnj1423  29689  bnj1452  29690  poimirlem2  31690  fdc  31822  orel  32087  lsatcvat  32369  lkrpssN  32482  2at0mat0  32843  atmod1i1m  33176  lhp2at0nle  33353  trlcone  34048  tendoex  34295  dihlspsnssN  34653  dochkrsm  34779  lcfl8  34823  lclkrlem2b  34829  lclkrlem2s  34846  lcfrlem21  34884  mapdval2N  34951  mapdspex  34989  pell1qrgaplem  35473  monotoddzzfi  35544  oddcomabszz  35546  zindbi  35548  rmxnn  35555  jm2.24  35567  acongeq  35587  jm2.23  35605  jm2.26lem3  35610  wepwsolem  35654  frege102d  36033  fnchoice  37038  refsum2cnlem1  37046  wallispilem3  37546  wtgoldbnnsum4prm  38344  bgoldbnnsum3prm  38346  nn0sumshdiglem1  39250
  Copyright terms: Public domain W3C validator