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

Theorem mpjaod 718
Description: Eliminate a disjunction in a deduction. (Contributed by Mario Carneiro, 29-May-2016.)
Hypotheses
Ref Expression
jaod.1 (𝜑 → (𝜓𝜒))
jaod.2 (𝜑 → (𝜃𝜒))
jaod.3 (𝜑 → (𝜓𝜃))
Assertion
Ref Expression
mpjaod (𝜑𝜒)

Proof of Theorem mpjaod
StepHypRef Expression
1 jaod.3 . 2 (𝜑 → (𝜓𝜃))
2 jaod.1 . . 3 (𝜑 → (𝜓𝜒))
3 jaod.2 . . 3 (𝜑 → (𝜃𝜒))
42, 3jaod 717 . 2 (𝜑 → ((𝜓𝜃) → 𝜒))
51, 4mpd 13 1 (𝜑𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wo 708
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  ifbothdc  3566  opth1  4232  onsucelsucexmidlem  4524  reldmtpos  6247  dftpos4  6257  nnm00  6524  xpfi  6922  omp1eomlem  7086  ctmlemr  7100  ctssdclemn0  7102  finomni  7131  indpi  7319  enq0tr  7411  prarloclem3step  7473  distrlem4prl  7561  distrlem4pru  7562  lelttr  8023  nn1suc  8914  nnsub  8934  nn0lt2  9310  uzin  9536  xrlelttr  9780  xlesubadd  9857  fzfig  10403  seq3id  10481  seq3z  10484  faclbnd  10692  facavg  10697  bcval5  10714  hashfzo  10773  iserex  11318  fsum3cvg  11357  fsumf1o  11369  fisumss  11371  fsumcl2lem  11377  fsumadd  11385  fsummulc2  11427  isumsplit  11470  fprodf1o  11567  prodssdc  11568  fprodssdc  11569  fprodmul  11570  absdvdsb  11787  dvdsabsb  11788  dvdsabseq  11823  m1exp1  11876  flodddiv4  11909  gcdaddm  11955  gcdabs1  11960  lcmdvds  12049  prmind2  12090  rpexp  12123  fermltl  12204  pcxnn0cl  12280  pcxcl  12281  pcabs  12295  pcmpt  12311  pockthg  12325  mulgnn0ass  12894  trilpolemcl  14408  trilpolemlt1  14412
  Copyright terms: Public domain W3C validator