ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpjaodan GIF version

Theorem mpjaodan 745
Description: Eliminate a disjunction in a deduction. A translation of natural deduction rule E ( elimination). (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 744 . 2 ((𝜑 ∧ (𝜓𝜃)) → 𝜒)
51, 4mpdan 412 1 (𝜑𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wo 662
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  mpjao3dan  1239  ifcldadc  3400  ifeq1dadc  3401  ifbothdadc  3402  ifcldcd  3405  exmidundif  3998  ordtri2or2exmidlem  4304  reg2exmidlema  4312  frecabcl  6095  nnsucuniel  6187  dcdifsnid  6194  phpm  6510  fidifsnen  6515  dif1enen  6525  fin0  6530  finexdc  6544  en2eqpr  6549  fientri3  6551  unsnfidcex  6556  unsnfidcel  6557  undifdcss  6559  ssfirab  6567  finomni  6700  exmidfodomrlemeldju  6727  exmidfodomrlemreseldju  6728  exmidfodomrlemr  6730  exmidfodomrlemrALT  6731  mullocprlem  7031  recexprlemloc  7092  nnnninf  8644  z2ge  9182  fztri3or  9347  fzm1  9406  fzneuz  9407  exfzdc  9539  exbtwnzlemstep  9547  rebtwn2zlemstep  9552  apbtwnz  9569  modifeq2int  9681  modsumfzodifsn  9691  expaddzaplem  9834  expnbnd  9911  bcval  9991  bccmpl  9996  ibcval5  10005  bcpasc  10008  bccl  10009  hashennnuni  10021  hashnncl  10038  resqrexlemnm  10277  resqrexlemcvg  10278  resqrexlemoverl  10280  resqrexlemglsq  10281  leabs  10333  nn0abscl  10344  ltabs  10346  abslt  10347  fzomaxdif  10372  maxleim  10464  maxabslemval  10467  minmax  10485  sumdc  10568  isumrb  10574  dvdsle  10624  mod2eq1n2dvds  10658  zsupcllemstep  10720  infssuzex  10724  gcdsupex  10728  gcdsupcl  10729  gcdval  10730  gcddvds  10734  gcdcl  10737  gcd0id  10749  gcdneg  10752  bezoutlemmain  10766  bezoutlemzz  10770  bezoutlemaz  10771  bezoutlembz  10772  dfgcd3  10778  dfgcd2  10782  nn0seqcvgd  10802  eucalgf  10816  eucalginv  10817  dvdslcm  10830  lcmcl  10833  lcmneg  10835  lcmgcd  10839  lcmdvds  10840  lcmid  10841  mulgcddvds  10855  pw2dvdslemn  10922  sqrt2irrap  10937  phibndlem  10971
  Copyright terms: Public domain W3C validator