Theorem mpjaodan 973

Description: Eliminate a disjunction in a deduction. A translation of natural deduction rule ∨ E (∨ elimination), see natded 30791. (Contributed by Mario Carneiro, 29-May-2016.)

Hypotheses

Ref	Expression
jaodan.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)
jaodan.2	⊢ ((𝜑 ∧ 𝜃) → 𝜒)
jaodan.3	⊢ (𝜑 → (𝜓 ∨ 𝜃))

Assertion

Ref	Expression
mpjaodan	⊢ (𝜑 → 𝜒)

Proof of Theorem mpjaodan

Step	Hyp	Ref	Expression
1		jaodan.3	. 2 ⊢ (𝜑 → (𝜓 ∨ 𝜃))
2		jaodan.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3		jaodan.2	. . 3 ⊢ ((𝜑 ∧ 𝜃) → 𝜒)
4	2, 3	jaodan 972	. 2 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃)) → 𝜒)
5	1, 4	mpdan 700	1 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862

This theorem is used by:  onunel  6475  weniso  7365  isf32lem2  10356  isf32lem4  10358  fpwwe2lem10  10643  fpwwe2lem11  10644  lecasei  11334  ltlecasei  11336  xaddass  13293  xlesubadd  13307  xmulge0  13328  xadddi2  13341  xrsupss  13353  xrinfmss  13354  fzm1  13654  seqf1olem2  14098  expaddzlem  14161  discr  14296  sgncl  15160  sgnmul  15170  fzomaxdif  15421  iseralt  15762  sumrb  15790  telfsumo  15880  fsumparts  15884  ntrivcvgtail  15980  prodrb  16012  bitsf1  16529  smupvallem  16566  eucalgf  16666  eucalginv  16667  vdwmc2  17064  fvprif  17640  mreexmrid  17724  mreexexlem3d  17727  chnub  18703  chnccats1  18706  chnccat  18707  mulgfval  19166  ressmulgnn0  19174  mulgnn0p1  19182  mulgnn0subcl  19184  mulgsubcl  19185  mulgneg  19189  mulgz  19199  mulgnn0dir  19201  mulgdirlem  19202  mulgdir  19203  submmulg  19215  ghmmulg  19329  odid  19639  oddvds  19648  dfod2  19665  gexid  19682  gexdvds  19685  mulgnn0di  19926  mulgdi  19927  gsumzsplit  20028  2nsgsimpgd  20205  prmgrpsimpgd  20217  lringuplu  20680  lsppratlem5  21312  ssdifidllem  21521  prmirred  21661  mhpmulcl  22349  1stckgenlem  23747  qtoprest  23911  tgpmulg  24287  tsmssplit  24346  xblss2ps  24595  xblss2  24596  metustfbas  24751  nmoix  24923  nmoleub  24925  idnghm  24937  blcvx  24992  icccmp  25020  xrge0tsms  25029  metdstri  25046  nmoleub2lem  25310  rrxcph  25588  rrxdstprj1  25605  ivthle  25652  ivthle2  25653  dyadmbl  25796  volivth  25803  itg2const2  25937  itg2mulc  25943  dvlip2  26191  dvfsumlem1  26222  mdegmullem  26272  coemulhi  26448  dgrcolem2  26468  coseq00topi  26704  abssinper  26723  cxplea  26898  cxple2  26899  cxple2a  26901  cxpcn3  26950  cxpaddlelem  26953  cxpaddle  26954  ang180lem3  27013  dcubic2  27046  birthdaylem2  27154  jensen  27190  ppiltx  27378  chtub  27413  bcmono  27478  bcmax  27479  bpos  27494  lgseisenlem1  27576  2sqlem4  27622  2sqmod  27637  pntrlog2bndlem5  27782  pntpbnd1  27787  noinfbnd2lem1  27931  noetasuplem4  27937  noetainflem4  27941  mulsproplem12  28357  mulsproplem13  28358  mulsproplem14  28359  lemulsd  28368  mulsge0d  28376  mulscan2d  28409  lemuls1ad  28412  absmuls  28474  absnegs  28477  leabss  28478  tgldimor  28808  tgifscgr  28814  tgcgrxfr  28824  tgbtwnconn1  28881  tgbtwnconn2  28882  tgbtwnconn3  28883  tgbtwnconnln3  28884  tgbtwnconn22  28885  tgbtwnconnln1  28886  tgbtwnconnln2  28887  legtrid  28897  legbtwn  28900  tgcgrsub2  28901  legov3  28904  hlln  28916  hltr  28919  btwnhl  28923  ncolncol  28957  mirconn  28992  krippen  29005  midexlem  29006  midex  29055  opphllem2  29066  opphllem5  29069  opphllem6  29070  outpasch  29074  hlpasch  29075  plngcplem  29104  plngrotlem1  29106  plngrotlem2  29107  lnssplng  29111  trgcopyeulem  29153  cgrahl  29175  cgracol  29176  prlngmolem2  29240  ex-natded5.7  30799  ex-natded5.13  30803  ex-natded9.20  30805  ex-natded9.20-2  30806  fconst7v  33002  suppovss  33063  nn0mnfxrd  33133  xrge0infss  33142  xnn0gt0  33151  nn0xmulclb  33153  difioo  33164  iundisjcnt  33180  f1ocnt  33182  fzo0opth  33185  hashxpe  33189  nexple  33214  2exple2exp  33215  ccatws1f1o  33304  xrsmulgzz  33360  xrge0addgt0  33368  xrge0adddir  33369  ressmulgnn0d  33395  xrge0tsmsd  33424  gsumwun  33427  tocyc01  33469  cycpmco2lem4  33480  cycpmco2lem7  33483  cycpmco2  33484  cyc3co2  33491  cycpmrn  33494  archirngz  33540  archiabllem2a  33545  elrgspnlem2  33594  ssmxidllem  33787  rprmirred  33852  rprmdvdspow  33854  1arithufdlem3  33867  dfufd2lem  33870  ply1dg3rt0irred  33905  esplyfval1  33994  lindsun  34046  lbsdiflsp0  34047  fldextrspunlsplem  34094  constrmon  34165  constrconj  34166  constrfin  34167  constrelextdg2  34168  constrextdg2lem  34169  zconstr  34185  submateq  34230  lmat22lem  34238  locfinref  34262  xrge0mulc1cn  34362  zrhcntr  34400  qqhval2lem  34402  esumpcvgval  34499  esumcvg  34507  sigaclcu3  34543  measiuns  34639  voliune  34651  volfiniune  34652  volmeas  34653  gsumnunsn  34963  signsply0  34970  signswch  34980  signslema  34981  signstfvneq0  34991  chtvalz  35048  btwnlng13  35089  bnj517  35305  bnj1408  35456  bnj1423  35471  bnj1452  35472  weiunse  37020  dnibndlem13  37120  dnibnd  37121  irrdifflemf  38010  poimirlem2  38314  fdc  38437  orel  38792  lsatcvat  39865  lkrpssN  39978  2at0mat0  40340  atmod1i1m  40673  lhp2at0nle  40850  trlcone  41543  tendoex  41790  dihlspsnssN  42147  dochkrsm  42273  lcfl8  42317  lclkrlem2b  42323  lclkrlem2s  42340  lcfrlem21  42378  mapdval2N  42445  mapdspex  42483  aks4d1p5  42888  hashnexinjle  42937  sticksstones12a  42965  sticksstones13  42967  sn-msqgt0d  43301  fimgmcyclem  43342  fsuppind  43363  flt4lem7  43432  nna4b4nsq  43433  pell1qrgaplem  43641  monotoddzzfi  43710  oddcomabszz  43712  zindbi  43714  rmxnn  43719  jm2.24  43731  acongeq  43751  jm2.23  43764  jm2.26lem3  43769  wepwsolem  43810  oe0rif  44053  onmcl  44099  omabs2  44100  omcl2  44101  onsucunipr  44140  oaun3lem1  44142  fzuntgd  44225  frege102d  44521  fnchoice  45790  refsum2cnlem1  45798  wallispilem3  46822  chnsubseqwl  47636  squeezedltsq  47644  wtgoldbnnsum4prm  48608  bgoldbnnsum3prm  48610  nn0sumshdiglem1  49442  mofeu  49667  toslat  49801  2arwcatlem2  50415  2arwcatlem3  50416  2arwcatlem4  50417  2arwcatlem5  50418  2arwcat  50419