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

Theorem mpjao3dan 1289
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 787 . 2  |-  ( (
ph  /\  ( ps  \/  th ) )  ->  ch )
4 mpjao3dan.3 . 2  |-  ( (
ph  /\  ta )  ->  ch )
5 mpjao3dan.4 . . 3  |-  ( ph  ->  ( ps  \/  th  \/  ta ) )
6 df-3or 964 . . 3  |-  ( ( ps  \/  th  \/  ta )  <->  ( ( ps  \/  th )  \/ 
ta ) )
75, 6sylib 121 . 2  |-  ( ph  ->  ( ( ps  \/  th )  \/  ta )
)
83, 4, 7mpjaodan 788 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    \/ wo 698    \/ w3o 962
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699
This theorem depends on definitions:  df-bi 116  df-3or 964
This theorem is referenced by:  wetriext  4536  nntri3  6444  nntri2or2  6445  nntr2  6450  tridc  6844  nnnninfeq  7071  exmidontriimlem2  7157  caucvgprlemnkj  7586  caucvgprlemnbj  7587  caucvgprprlemnkj  7612  caucvgprprlemnbj  7613  caucvgsr  7722  npnflt  9719  nmnfgt  9722  xleadd1a  9777  xltadd1  9780  xlt2add  9784  xsubge0  9785  xleaddadd  9791  addmodlteq  10297  iseqf1olemkle  10383  hashfiv01gt1  10656  xrmaxltsup  11155  xrmaxadd  11158  xrbdtri  11173  cvgratz  11429  zdvdsdc  11707  divalglemeunn  11811  divalglemex  11812  divalglemeuneg  11813  divalg  11814  znege1  12052  ennnfonelemk  12129  isxmet2d  12748  trilpolemres  13613  trirec0  13615
  Copyright terms: Public domain W3C validator