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

Theorem orbi1rVD 33770
Description: Virtual deduction proof of orbi1r 33401. 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 )  ->.  ( ch  \/  ph ) ).
3:2,?: e2 33539  |-  (. ( ph  <->  ps ) ,. ( ch  \/  ph )  ->.  ( ph  \/  ch ) ).
4:1,3,?: e12 33643  |-  (. ( ph  <->  ps ) ,. ( ch  \/  ph )  ->.  ( ps  \/  ch ) ).
5:4,?: e2 33539  |-  (. ( ph  <->  ps ) ,. ( ch  \/  ph )  ->.  ( ch  \/  ps ) ).
6:5:  |-  (. ( ph  <->  ps )  ->.  ( ( ch  \/  ph )  ->  ( ch  \/  ps ) ) ).
7::  |-  (. ( ph  <->  ps ) ,. ( ch  \/  ps )  ->.  ( ch  \/  ps ) ).
8:7,?: e2 33539  |-  (. ( ph  <->  ps ) ,. ( ch  \/  ps )  ->.  ( ps  \/  ch ) ).
9:1,8,?: e12 33643  |-  (. ( ph  <->  ps ) ,. ( ch  \/  ps )  ->.  ( ph  \/  ch ) ).
10:9,?: e2 33539  |-  (. ( ph  <->  ps ) ,. ( ch  \/  ps )  ->.  ( ch  \/  ph ) ).
11:10:  |-  (. ( ph  <->  ps )  ->.  ( ( ch  \/  ps )  ->  ( ch  \/  ph ) ) ).
12:6,11,?: e11 33596  |-  (. ( ph  <->  ps )  ->.  ( ( ch  \/  ph )  <->  ( ch  \/  ps ) ) ).
qed:12:  |-  ( ( ph  <->  ps )  ->  ( ( ch  \/  ph )  <->  ( ch  \/  ps ) ) )
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
orbi1rVD  |-  ( (
ph 
<->  ps )  ->  (
( ch  \/  ph ) 
<->  ( ch  \/  ps ) ) )

Proof of Theorem orbi1rVD
StepHypRef Expression
1 idn1 33473 . . . . . 6  |-  (. ( ph 
<->  ps )  ->.  ( ph  <->  ps ) ).
2 idn2 33521 . . . . . . 7  |-  (. ( ph 
<->  ps ) ,. ( ch  \/  ph )  ->.  ( ch  \/  ph ) ).
3 pm1.4 386 . . . . . . 7  |-  ( ( ch  \/  ph )  ->  ( ph  \/  ch ) )
42, 3e2 33539 . . . . . 6  |-  (. ( ph 
<->  ps ) ,. ( ch  \/  ph )  ->.  ( ph  \/  ch ) ).
5 orbi1 705 . . . . . . 7  |-  ( (
ph 
<->  ps )  ->  (
( ph  \/  ch ) 
<->  ( ps  \/  ch ) ) )
65biimpd 207 . . . . . 6  |-  ( (
ph 
<->  ps )  ->  (
( ph  \/  ch )  ->  ( ps  \/  ch ) ) )
71, 4, 6e12 33643 . . . . 5  |-  (. ( ph 
<->  ps ) ,. ( ch  \/  ph )  ->.  ( ps  \/  ch ) ).
8 pm1.4 386 . . . . 5  |-  ( ( ps  \/  ch )  ->  ( ch  \/  ps ) )
97, 8e2 33539 . . . 4  |-  (. ( ph 
<->  ps ) ,. ( ch  \/  ph )  ->.  ( ch  \/  ps ) ).
109in2 33513 . . 3  |-  (. ( ph 
<->  ps )  ->.  ( ( ch  \/  ph )  -> 
( ch  \/  ps ) ) ).
11 idn2 33521 . . . . . . 7  |-  (. ( ph 
<->  ps ) ,. ( ch  \/  ps )  ->.  ( ch  \/  ps ) ).
12 pm1.4 386 . . . . . . 7  |-  ( ( ch  \/  ps )  ->  ( ps  \/  ch ) )
1311, 12e2 33539 . . . . . 6  |-  (. ( ph 
<->  ps ) ,. ( ch  \/  ps )  ->.  ( ps  \/  ch ) ).
145biimprd 223 . . . . . 6  |-  ( (
ph 
<->  ps )  ->  (
( ps  \/  ch )  ->  ( ph  \/  ch ) ) )
151, 13, 14e12 33643 . . . . 5  |-  (. ( ph 
<->  ps ) ,. ( ch  \/  ps )  ->.  ( ph  \/  ch ) ).
16 pm1.4 386 . . . . 5  |-  ( (
ph  \/  ch )  ->  ( ch  \/  ph ) )
1715, 16e2 33539 . . . 4  |-  (. ( ph 
<->  ps ) ,. ( ch  \/  ps )  ->.  ( ch  \/  ph ) ).
1817in2 33513 . . 3  |-  (. ( ph 
<->  ps )  ->.  ( ( ch  \/  ps )  -> 
( ch  \/  ph ) ) ).
19 bi3 187 . . 3  |-  ( ( ( ch  \/  ph )  ->  ( ch  \/  ps ) )  ->  (
( ( ch  \/  ps )  ->  ( ch  \/  ph ) )  ->  ( ( ch  \/  ph )  <->  ( ch  \/  ps ) ) ) )
2010, 18, 19e11 33596 . 2  |-  (. ( ph 
<->  ps )  ->.  ( ( ch  \/  ph )  <->  ( ch  \/  ps ) ) ).
2120in1 33470 1  |-  ( (
ph 
<->  ps )  ->  (
( ch  \/  ph ) 
<->  ( ch  \/  ps ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    \/ wo 368
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-vd1 33469  df-vd2 33477
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator