Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  3ornot23VD Structured version   Unicode version

Theorem 3ornot23VD 32745
Description: Virtual deduction proof of 3ornot23 32375. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.
1::
 |-  (. ( -.  ph  /\  -.  ps )  ->.  ( -.  ph  /\  -.  ps ) ).
2::  |-  (. ( -.  ph  /\  -.  ps ) ,. ( ch  \/  ph  \/  ps )  ->.  ( ch  \/  ph  \/  ps ) ).
3:1,?: e1a 32511  |-  (. ( -.  ph  /\  -.  ps )  ->.  -.  ph ).
4:1,?: e1a 32511  |-  (. ( -.  ph  /\  -.  ps )  ->.  -.  ps ).
5:3,4,?: e11 32572  |-  (. ( -.  ph  /\  -.  ps )  ->.  -.  ( ph  \/  ps ) ).
6:2,?: e2 32515  |-  (. ( -.  ph  /\  -.  ps ) ,. ( ch  \/  ph  \/  ps )  ->.  ( ch  \/  ( ph  \/  ps ) ) ).
7:5,6,?: e12 32619  |-  (. ( -.  ph  /\  -.  ps ) ,. ( ch  \/  ph  \/  ps )  ->.  ch ).
8:7:  |-  (. ( -.  ph  /\  -.  ps )  ->.  ( ( ch  \/  ph  \/  ps )  ->  ch ) ).
qed:8:  |-  ( ( -.  ph  /\  -.  ps )  ->  ( ( ch  \/  ph  \/  ps )  ->  ch ) )
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
3ornot23VD  |-  ( ( -.  ph  /\  -.  ps )  ->  ( ( ch  \/  ph  \/  ps )  ->  ch ) )

Proof of Theorem 3ornot23VD
StepHypRef Expression
1 idn1 32449 . . . . . 6  |-  (. ( -.  ph  /\  -.  ps ) 
->.  ( -.  ph  /\  -.  ps ) ).
2 simpl 457 . . . . . 6  |-  ( ( -.  ph  /\  -.  ps )  ->  -.  ph )
31, 2e1a 32511 . . . . 5  |-  (. ( -.  ph  /\  -.  ps ) 
->.  -.  ph ).
4 simpr 461 . . . . . 6  |-  ( ( -.  ph  /\  -.  ps )  ->  -.  ps )
51, 4e1a 32511 . . . . 5  |-  (. ( -.  ph  /\  -.  ps ) 
->.  -.  ps ).
6 ioran 490 . . . . . 6  |-  ( -.  ( ph  \/  ps ) 
<->  ( -.  ph  /\  -.  ps ) )
76simplbi2 625 . . . . 5  |-  ( -. 
ph  ->  ( -.  ps  ->  -.  ( ph  \/  ps ) ) )
83, 5, 7e11 32572 . . . 4  |-  (. ( -.  ph  /\  -.  ps ) 
->.  -.  ( ph  \/  ps ) ).
9 idn2 32497 . . . . 5  |-  (. ( -.  ph  /\  -.  ps ) ,. ( ch  \/  ph  \/  ps )  ->.  ( ch  \/  ph  \/  ps ) ).
10 3orass 976 . . . . . 6  |-  ( ( ch  \/  ph  \/  ps )  <->  ( ch  \/  ( ph  \/  ps )
) )
1110biimpi 194 . . . . 5  |-  ( ( ch  \/  ph  \/  ps )  ->  ( ch  \/  ( ph  \/  ps ) ) )
129, 11e2 32515 . . . 4  |-  (. ( -.  ph  /\  -.  ps ) ,. ( ch  \/  ph  \/  ps )  ->.  ( ch  \/  ( ph  \/  ps ) ) ).
13 orel2 383 . . . 4  |-  ( -.  ( ph  \/  ps )  ->  ( ( ch  \/  ( ph  \/  ps ) )  ->  ch ) )
148, 12, 13e12 32619 . . 3  |-  (. ( -.  ph  /\  -.  ps ) ,. ( ch  \/  ph  \/  ps )  ->.  ch ).
1514in2 32489 . 2  |-  (. ( -.  ph  /\  -.  ps ) 
->.  ( ( ch  \/  ph  \/  ps )  ->  ch ) ).
1615in1 32446 1  |-  ( ( -.  ph  /\  -.  ps )  ->  ( ( ch  \/  ph  \/  ps )  ->  ch ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 368    /\ wa 369    \/ w3o 972
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-vd1 32445  df-vd2 32453
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator