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

Theorem mpjao3dan 1268
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 769 . 2  |-  ( (
ph  /\  ( ps  \/  th ) )  ->  ch )
4 mpjao3dan.3 . 2  |-  ( (
ph  /\  ta )  ->  ch )
5 mpjao3dan.4 . . 3  |-  ( ph  ->  ( ps  \/  th  \/  ta ) )
6 df-3or 946 . . 3  |-  ( ( ps  \/  th  \/  ta )  <->  ( ( ps  \/  th )  \/ 
ta ) )
75, 6sylib 121 . 2  |-  ( ph  ->  ( ( ps  \/  th )  \/  ta )
)
83, 4, 7mpjaodan 770 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    \/ wo 680    \/ w3o 944
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 681
This theorem depends on definitions:  df-bi 116  df-3or 946
This theorem is referenced by:  wetriext  4459  nntri3  6359  nntri2or2  6360  nntr2  6365  tridc  6759  caucvgprlemnkj  7438  caucvgprlemnbj  7439  caucvgprprlemnkj  7464  caucvgprprlemnbj  7465  caucvgsr  7574  npnflt  9549  nmnfgt  9552  xleadd1a  9607  xltadd1  9610  xlt2add  9614  xsubge0  9615  xleaddadd  9621  addmodlteq  10122  iseqf1olemkle  10208  hashfiv01gt1  10479  xrmaxltsup  10978  xrmaxadd  10981  xrbdtri  10996  cvgratz  11252  zdvdsdc  11421  divalglemeunn  11525  divalglemex  11526  divalglemeuneg  11527  divalg  11528  znege1  11762  ennnfonelemk  11819  isxmet2d  12423  nninfalllemn  13036  trilpolemres  13069
  Copyright terms: Public domain W3C validator