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

Theorem mpjaod 671
 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 670 . 2 (𝜑 → ((𝜓𝜃) → 𝜒))
51, 4mpd 13 1 (𝜑𝜒)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∨ 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:  ifbothdc  3388  opth1  3999  onsucelsucexmidlem  4280  reldmtpos  5902  dftpos4  5912  nnm00  6168  indpi  6594  enq0tr  6686  prarloclem3step  6748  distrlem4prl  6836  distrlem4pru  6837  lelttr  7266  nn1suc  8125  nnsub  8144  nn0lt2  8510  uzin  8732  xrlelttr  8952  fzfig  9512  iseqid  9563  iseqz  9566  expival  9575  faclbnd  9765  facavg  9770  ibcval5  9787  iiserex  10315  fisumcvg  10338  absdvdsb  10358  dvdsabsb  10359  dvdsabseq  10392  m1exp1  10445  flodddiv4  10478  gcdaddm  10519  gcdabs1  10524  lcmdvds  10605  prmind2  10646  rpexp  10676
 Copyright terms: Public domain W3C validator