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

Theorem mpjaod 637
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 636 . 2 (φ → ((ψ θ) → χ))
51, 4mpd 13 1 (φχ)
Colors of variables: wff set class
Syntax hints:  wi 4   wo 628
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 629
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  opth1  3964  onsucelsucexmidlem  4214  reldmtpos  5809  dftpos4  5819  nnm00  6038  indpi  6326  enq0tr  6416  prarloclem3step  6478  distrlem4prl  6559  distrlem4pru  6560  lelttr  6883  nn1suc  7694  nnsub  7713  nn0lt2  8078  uzin  8261  xrlelttr  8472  fzfig  8867  expival  8891
  Copyright terms: Public domain W3C validator