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

Theorem mpjao3dan 1320
Description: Eliminate a 3-way disjunction in a deduction. (Contributed by Thierry Arnoux, 13-Apr-2018.)
Hypotheses
Ref Expression
mpjao3dan.1  |-  ( (
ph  /\  ps )  ->  ch )
mpjao3dan.2  |-  ( (
ph  /\  th )  ->  ch )
mpjao3dan.3  |-  ( (
ph  /\  ta )  ->  ch )
mpjao3dan.4  |-  ( ph  ->  ( ps  \/  th  \/  ta ) )
Assertion
Ref Expression
mpjao3dan  |-  ( ph  ->  ch )

Proof of Theorem mpjao3dan
StepHypRef Expression
1 mpjao3dan.1 . . 3  |-  ( (
ph  /\  ps )  ->  ch )
2 mpjao3dan.2 . . 3  |-  ( (
ph  /\  th )  ->  ch )
31, 2jaodan 799 . 2  |-  ( (
ph  /\  ( ps  \/  th ) )  ->  ch )
4 mpjao3dan.3 . 2  |-  ( (
ph  /\  ta )  ->  ch )
5 mpjao3dan.4 . . 3  |-  ( ph  ->  ( ps  \/  th  \/  ta ) )
6 df-3or 982 . . 3  |-  ( ( ps  \/  th  \/  ta )  <->  ( ( ps  \/  th )  \/ 
ta ) )
75, 6sylib 122 . 2  |-  ( ph  ->  ( ( ps  \/  th )  \/  ta )
)
83, 4, 7mpjaodan 800 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    \/ wo 710    \/ w3o 980
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711
This theorem depends on definitions:  df-bi 117  df-3or 982
This theorem is referenced by:  wetriext  4625  nntri3  6583  nntri2or2  6584  nntr2  6589  tridc  6996  nnnninfeq  7230  exmidontriimlem2  7334  caucvgprlemnkj  7779  caucvgprlemnbj  7780  caucvgprprlemnkj  7805  caucvgprprlemnbj  7806  caucvgsr  7915  npnflt  9937  nmnfgt  9940  xleadd1a  9995  xltadd1  9998  xlt2add  10002  xsubge0  10003  xleaddadd  10009  addmodlteq  10543  iseqf1olemkle  10642  hashfiv01gt1  10927  iswrdiz  11001  xrmaxltsup  11569  xrmaxadd  11572  xrbdtri  11587  cvgratz  11843  zdvdsdc  12123  divalglemeunn  12232  divalglemex  12233  divalglemeuneg  12234  divalg  12235  znege1  12500  ennnfonelemk  12771  isxmet2d  14820  trilpolemres  15981  trirec0  15983
  Copyright terms: Public domain W3C validator