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

Theorem mpjaodan 862
Description: Eliminate a disjunction in a deduction. A translation of natural deduction rule E ( elimination), see natded 27592. (Contributed by Mario Carneiro, 29-May-2016.)
Hypotheses
Ref Expression
jaodan.1 ((𝜑𝜓) → 𝜒)
jaodan.2 ((𝜑𝜃) → 𝜒)
jaodan.3 (𝜑 → (𝜓𝜃))
Assertion
Ref Expression
mpjaodan (𝜑𝜒)

Proof of Theorem mpjaodan
StepHypRef Expression
1 jaodan.3 . 2 (𝜑 → (𝜓𝜃))
2 jaodan.1 . . 3 ((𝜑𝜓) → 𝜒)
3 jaodan.2 . . 3 ((𝜑𝜃) → 𝜒)
42, 3jaodan 861 . 2 ((𝜑 ∧ (𝜓𝜃)) → 𝜒)
51, 4mpdan 705 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 382  wa 383
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 384  df-an 385
This theorem is referenced by:  mpjao3dan  1544  weniso  6768  isf32lem2  9388  isf32lem4  9390  fpwwe2lem11  9674  fpwwe2lem12  9675  lecasei  10355  ltlecasei  10357  xaddass  12292  xlesubadd  12306  xmulge0  12327  xadddi2  12340  xrsupss  12352  xrinfmss  12353  fzm1  12633  seqf1olem2  13055  expaddzlem  13117  discr  13215  fzomaxdif  14302  iseralt  14634  sumrb  14663  telfsumo  14753  fsumparts  14757  ntrivcvgtail  14851  prodrb  14881  bitsf1  15390  smupvallem  15427  eucalgf  15518  eucalginv  15519  vdwmc2  15905  mreexmrid  16525  mreexexlem3d  16528  mulgnn0p1  17773  mulgnn0subcl  17775  mulgsubcl  17776  mulgneg  17781  mulgz  17789  mulgnn0dir  17792  mulgdirlem  17793  mulgdir  17794  submmulg  17807  ghmmulg  17893  odid  18177  oddvds  18186  dfod2  18201  gexid  18216  gexdvds  18219  mulgnn0di  18451  mulgdi  18452  gsumzsplit  18547  lsppratlem5  19373  prmirred  20065  1stckgenlem  21578  qtoprest  21742  tgpmulg  22118  tsmssplit  22176  xblss2ps  22427  xblss2  22428  metustfbas  22583  nmoix  22754  nmoleub  22756  idnghm  22768  blcvx  22822  icccmp  22849  xrge0tsms  22858  metdstri  22875  nmoleub2lem  23134  rrxcph  23400  rrxdstprj1  23412  ivthle  23445  ivthle2  23446  dyadmbl  23588  volivth  23595  itg2const2  23727  itg2mulc  23733  dvlip2  23977  dvfsumlem1  24008  mdegmullem  24057  coemulhi  24229  dgrcolem2  24249  coseq00topi  24474  abssinper  24490  cxplea  24662  cxple2  24663  cxple2a  24665  cxpcn3  24709  cxpaddlelem  24712  cxpaddle  24713  ang180lem3  24761  dcubic2  24791  birthdaylem2  24899  jensen  24935  ppiltx  25123  chtub  25157  bcmono  25222  bcmax  25223  bpos  25238  lgseisenlem1  25320  2sqlem4  25366  pntrlog2bndlem5  25490  pntpbnd1  25495  tgldimor  25617  tgifscgr  25623  tgcgrxfr  25633  tgbtwnconn1  25690  tgbtwnconn2  25691  tgbtwnconn3  25692  tgbtwnconnln3  25693  tgbtwnconn22  25694  tgbtwnconnln1  25695  tgbtwnconnln2  25696  legtrid  25706  legbtwn  25709  tgcgrsub2  25710  legov3  25713  hlln  25722  hltr  25725  btwnhl  25729  ncolncol  25761  mirconn  25793  krippen  25806  midexlem  25807  midex  25849  opphllem2  25860  opphllem5  25863  opphllem6  25864  outpasch  25867  hlpasch  25868  trgcopyeulem  25917  cgrahl  25938  cgracol  25939  ex-natded5.7  27600  ex-natded5.13  27604  ex-natded9.20  27606  ex-natded9.20-2  27607  xrge0infss  29855  difioo  29874  iundisjcnt  29887  f1ocnt  29889  2sqmod  29978  xrsmulgzz  30008  ressmulgnn0  30014  xrge0addgt0  30021  xrge0adddir  30022  archirngz  30073  archiabllem2a  30078  xrge0tsmsd  30115  submateq  30205  lmat22lem  30213  locfinref  30238  xrge0mulc1cn  30317  qqhval2lem  30355  nexple  30401  esumpcvgval  30470  esumcvg  30478  sigaclcu3  30515  measiuns  30610  voliune  30622  volfiniune  30623  volmeas  30624  sgncl  30930  sgnmul  30934  gsumnunsn  30945  signsply0  30958  signswch  30968  signslema  30969  signstfvneq0  30979  chtvalz  31037  bnj517  31283  bnj1408  31432  bnj1423  31447  bnj1452  31448  noetalem3  32192  dnibndlem13  32807  dnibnd  32808  poimirlem2  33742  fdc  33872  orel  34235  lsatcvat  34858  lkrpssN  34971  2at0mat0  35332  atmod1i1m  35665  lhp2at0nle  35842  trlcone  36536  tendoex  36783  dihlspsnssN  37141  dochkrsm  37267  lcfl8  37311  lclkrlem2b  37317  lclkrlem2s  37334  lcfrlem21  37372  mapdval2N  37439  mapdspex  37477  pell1qrgaplem  37957  monotoddzzfi  38027  oddcomabszz  38029  zindbi  38031  rmxnn  38038  jm2.24  38050  acongeq  38070  jm2.23  38083  jm2.26lem3  38088  wepwsolem  38132  frege102d  38566  fnchoice  39705  refsum2cnlem1  39713  wallispilem3  40805  wtgoldbnnsum4prm  42218  bgoldbnnsum3prm  42220  nn0sumshdiglem1  42943
  Copyright terms: Public domain W3C validator