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

Theorem mpjaod 638
 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 637 . 2 (𝜑 → ((𝜓𝜃) → 𝜒))
51, 4mpd 13 1 (𝜑𝜒)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∨ wo 629 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  ifbothdc  3357  opth1  3973  onsucelsucexmidlem  4254  reldmtpos  5868  dftpos4  5878  nnm00  6102  indpi  6440  enq0tr  6532  prarloclem3step  6594  distrlem4prl  6682  distrlem4pru  6683  lelttr  7106  nn1suc  7933  nnsub  7952  nn0lt2  8322  uzin  8505  xrlelttr  8722  fzfig  9206  iseqid  9247  expival  9257  iiserex  9859
 Copyright terms: Public domain W3C validator