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

Theorem mpjaodan 711
Description: Eliminate a disjunction in a deduction. A translation of natural deduction rule  \/ E ( \/ elimination). (Contributed by Mario Carneiro, 29-May-2016.)
Hypotheses
Ref Expression
jaodan.1  |-  ( (
ph  /\  ps )  ->  ch )
jaodan.2  |-  ( (
ph  /\  th )  ->  ch )
jaodan.3  |-  ( ph  ->  ( ps  \/  th ) )
Assertion
Ref Expression
mpjaodan  |-  ( ph  ->  ch )

Proof of Theorem mpjaodan
StepHypRef Expression
1 jaodan.3 . 2  |-  ( ph  ->  ( ps  \/  th ) )
2 jaodan.1 . . 3  |-  ( (
ph  /\  ps )  ->  ch )
3 jaodan.2 . . 3  |-  ( (
ph  /\  th )  ->  ch )
42, 3jaodan 710 . 2  |-  ( (
ph  /\  ( ps  \/  th ) )  ->  ch )
51, 4mpdan 398 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 97    \/ 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:  mpjao3dan  1202  ifcldcd  3358  ordtri2or2exmidlem  4251  reg2exmidlema  4259  nndifsnid  6080  phpm  6327  fidifsnen  6331  fidifsnid  6332  fin0  6342  fientri3  6353  mullocprlem  6668  recexprlemloc  6729  z2ge  8739  fztri3or  8903  fzm1  8962  fzneuz  8963  qbtwnzlemstep  9103  rebtwn2zlemstep  9107  expaddzaplem  9298  expnbnd  9372  resqrexlemnm  9616  resqrexlemcvg  9617  resqrexlemoverl  9619  resqrexlemglsq  9620  leabs  9672  nn0abscl  9681  ltabs  9683  abslt  9684  fzomaxdif  9709  nn0seqcvgd  9880
  Copyright terms: Public domain W3C validator