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

Theorem mpjaod 673
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 672 . 2 (𝜑 → ((𝜓𝜃) → 𝜒))
51, 4mpd 13 1 (𝜑𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wo 664
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 665
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  ifbothdc  3419  opth1  4054  onsucelsucexmidlem  4335  reldmtpos  6000  dftpos4  6010  nnm00  6268  xpfi  6619  finomni  6775  indpi  6880  enq0tr  6972  prarloclem3step  7034  distrlem4prl  7122  distrlem4pru  7123  lelttr  7552  nn1suc  8413  nnsub  8432  nn0lt2  8798  uzin  9020  xrlelttr  9240  fzfig  9802  iseqid  9904  iseqz  9907  faclbnd  10113  facavg  10118  ibcval5  10135  hashfzo  10194  iserex  10690  fisumcvg  10729  fsumf1o  10744  fisumss  10746  fsumcl2lem  10753  fsumadd  10761  fsummulc2  10803  isumsplit  10845  absdvdsb  10894  dvdsabsb  10895  dvdsabseq  10928  m1exp1  10981  flodddiv4  11014  gcdaddm  11055  gcdabs1  11060  lcmdvds  11141  prmind2  11182  rpexp  11212
  Copyright terms: Public domain W3C validator