Theorem mpjaodan 827

Description: Eliminate a disjunction in a deduction. A translation of natural deduction rule \/ E ( \/ elimination), see natded 27260. (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

Step	Hyp	Ref	Expression
1		jaodan.3	. 2 |- ( ph -> ( ps \/ th ) )
2		jaodan.1	. . 3 |- ( ( ph /\ ps ) -> ch )
3		jaodan.2	. . 3 |- ( ( ph /\ th ) -> ch )
4	2, 3	jaodan 826	. 2 |- ( ( ph /\ ( ps \/ th ) ) -> ch )
5	1, 4	mpdan 702	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   \/ wo 383   /\ wa 384

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 197  df-or 385  df-an 386

This theorem is referenced by:  mpjao3dan  1395  weniso  6604  isf32lem2  9176  isf32lem4  9178  fpwwe2lem11  9462  fpwwe2lem12  9463  lecasei  10143  ltlecasei  10145  xaddass  12079  xlesubadd  12093  xmulge0  12114  xadddi2  12127  xrsupss  12139  xrinfmss  12140  fzm1  12420  seqf1olem2  12841  expaddzlem  12903  discr  13001  fzomaxdif  14083  iseralt  14415  sumrb  14444  telfsumo  14534  fsumparts  14538  ntrivcvgtail  14632  prodrb  14662  bitsf1  15168  smupvallem  15205  eucalgf  15296  eucalginv  15297  vdwmc2  15683  mreexmrid  16303  mreexexlem3d  16306  mulgnn0p1  17552  mulgnn0subcl  17554  mulgsubcl  17555  mulgneg  17560  mulgz  17568  mulgnn0dir  17571  mulgdirlem  17572  mulgdir  17573  submmulg  17586  ghmmulg  17672  odid  17957  oddvds  17966  dfod2  17981  gexid  17996  gexdvds  17999  mulgnn0di  18231  mulgdi  18232  gsumzsplit  18327  lsppratlem5  19151  prmirred  19843  1stckgenlem  21356  qtoprest  21520  tgpmulg  21897  tsmssplit  21955  xblss2ps  22206  xblss2  22207  metustfbas  22362  nmoix  22533  nmoleub  22535  idnghm  22547  blcvx  22601  icccmp  22628  xrge0tsms  22637  metdstri  22654  nmoleub2lem  22914  rrxcph  23180  rrxdstprj1  23192  ivthle  23225  ivthle2  23226  dyadmbl  23368  volivth  23375  itg2const2  23508  itg2mulc  23514  dvlip2  23758  dvfsumlem1  23789  mdegmullem  23838  coemulhi  24010  dgrcolem2  24030  coseq00topi  24254  abssinper  24270  cxplea  24442  cxple2  24443  cxple2a  24445  cxpcn3  24489  cxpaddlelem  24492  cxpaddle  24493  ang180lem3  24541  dcubic2  24571  birthdaylem2  24679  jensen  24715  ppiltx  24903  chtub  24937  bcmono  25002  bcmax  25003  bpos  25018  lgseisenlem1  25100  2sqlem4  25146  pntrlog2bndlem5  25270  pntpbnd1  25275  tgldimor  25397  tgifscgr  25403  tgcgrxfr  25413  tgbtwnconn1  25470  tgbtwnconn2  25471  tgbtwnconn3  25472  tgbtwnconnln3  25473  tgbtwnconn22  25474  tgbtwnconnln1  25475  tgbtwnconnln2  25476  legtrid  25486  legbtwn  25489  tgcgrsub2  25490  legov3  25493  hlln  25502  hltr  25505  btwnhl  25509  ncolncol  25541  mirconn  25573  krippen  25586  midexlem  25587  midex  25629  opphllem2  25640  opphllem5  25643  opphllem6  25644  outpasch  25647  hlpasch  25648  trgcopyeulem  25697  cgrahl  25718  cgracol  25719  ex-natded5.7  27268  ex-natded5.13  27272  ex-natded9.20  27274  ex-natded9.20-2  27275  xrge0infss  29525  difioo  29544  iundisjcnt  29557  f1ocnt  29559  2sqmod  29648  xrsmulgzz  29678  ressmulgnn0  29684  xrge0addgt0  29691  xrge0adddir  29692  archirngz  29743  archiabllem2a  29748  xrge0tsmsd  29785  submateq  29875  lmat22lem  29883  locfinref  29908  xrge0mulc1cn  29987  qqhval2lem  30025  nexple  30071  esumpcvgval  30140  esumcvg  30148  sigaclcu3  30185  measiuns  30280  voliune  30292  volfiniune  30293  volmeas  30294  sgncl  30600  sgnmul  30604  gsumnunsn  30615  signsply0  30628  signswch  30638  signslema  30639  signstfvneq0  30649  chtvalz  30707  bnj517  30955  bnj1408  31104  bnj1423  31119  bnj1452  31120  noetalem3  31865  dnibndlem13  32480  dnibnd  32481  poimirlem2  33411  fdc  33541  orel  33904  lsatcvat  34337  lkrpssN  34450  2at0mat0  34811  atmod1i1m  35144  lhp2at0nle  35321  trlcone  36016  tendoex  36263  dihlspsnssN  36621  dochkrsm  36747  lcfl8  36791  lclkrlem2b  36797  lclkrlem2s  36814  lcfrlem21  36852  mapdval2N  36919  mapdspex  36957  pell1qrgaplem  37437  monotoddzzfi  37507  oddcomabszz  37509  zindbi  37511  rmxnn  37518  jm2.24  37530  acongeq  37550  jm2.23  37563  jm2.26lem3  37568  wepwsolem  37612  frege102d  38046  fnchoice  39188  refsum2cnlem1  39196  wallispilem3  40284  wtgoldbnnsum4prm  41690  bgoldbnnsum3prm  41692  nn0sumshdiglem1  42415