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

Theorem orbi1rVD 28940
Description: Virtual deduction proof of orbi1r 28570. 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 28708  |-  (. ( ph  <->  ps ) ,. ( ch  \/  ph )  ->.  ( ph  \/  ch ) ).
4:1,3,?: e12 28813  |-  (. ( ph  <->  ps ) ,. ( ch  \/  ph )  ->.  ( ps  \/  ch ) ).
5:4,?: e2 28708  |-  (. ( ph  <->  ps ) ,. ( ch  \/  ph )  ->.  ( ch  \/  ps ) ).
6:5:  |-  (. ( ph  <->  ps )  ->.  ( ( ch  \/  ph )  ->  ( ch  \/  ps ) ) ).
7::  |-  (. ( ph  <->  ps ) ,. ( ch  \/  ps )  ->.  ( ch  \/  ps ) ).
8:7,?: e2 28708  |-  (. ( ph  <->  ps ) ,. ( ch  \/  ps )  ->.  ( ps  \/  ch ) ).
9:1,8,?: e12 28813  |-  (. ( ph  <->  ps ) ,. ( ch  \/  ps )  ->.  ( ph  \/  ch ) ).
10:9,?: e2 28708  |-  (. ( ph  <->  ps ) ,. ( ch  \/  ps )  ->.  ( ch  \/  ph ) ).
11:10:  |-  (. ( ph  <->  ps )  ->.  ( ( ch  \/  ps )  ->  ( ch  \/  ph ) ) ).
12:6,11,?: e11 28765  |-  (. ( 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 28641 . . . . . 6  |-  (. ( ph 
<->  ps )  ->.  ( ph  <->  ps ) ).
2 idn2 28690 . . . . . . 7  |-  (. ( ph 
<->  ps ) ,. ( ch  \/  ph )  ->.  ( ch  \/  ph ) ).
3 pm1.4 375 . . . . . . 7  |-  ( ( ch  \/  ph )  ->  ( ph  \/  ch ) )
42, 3e2 28708 . . . . . 6  |-  (. ( ph 
<->  ps ) ,. ( ch  \/  ph )  ->.  ( ph  \/  ch ) ).
5 orbi1 686 . . . . . . 7  |-  ( (
ph 
<->  ps )  ->  (
( ph  \/  ch ) 
<->  ( ps  \/  ch ) ) )
65biimpd 198 . . . . . 6  |-  ( (
ph 
<->  ps )  ->  (
( ph  \/  ch )  ->  ( ps  \/  ch ) ) )
71, 4, 6e12 28813 . . . . 5  |-  (. ( ph 
<->  ps ) ,. ( ch  \/  ph )  ->.  ( ps  \/  ch ) ).
8 pm1.4 375 . . . . 5  |-  ( ( ps  \/  ch )  ->  ( ch  \/  ps ) )
97, 8e2 28708 . . . 4  |-  (. ( ph 
<->  ps ) ,. ( ch  \/  ph )  ->.  ( ch  \/  ps ) ).
109in2 28682 . . 3  |-  (. ( ph 
<->  ps )  ->.  ( ( ch  \/  ph )  -> 
( ch  \/  ps ) ) ).
11 idn2 28690 . . . . . . 7  |-  (. ( ph 
<->  ps ) ,. ( ch  \/  ps )  ->.  ( ch  \/  ps ) ).
12 pm1.4 375 . . . . . . 7  |-  ( ( ch  \/  ps )  ->  ( ps  \/  ch ) )
1311, 12e2 28708 . . . . . 6  |-  (. ( ph 
<->  ps ) ,. ( ch  \/  ps )  ->.  ( ps  \/  ch ) ).
145biimprd 214 . . . . . 6  |-  ( (
ph 
<->  ps )  ->  (
( ps  \/  ch )  ->  ( ph  \/  ch ) ) )
151, 13, 14e12 28813 . . . . 5  |-  (. ( ph 
<->  ps ) ,. ( ch  \/  ps )  ->.  ( ph  \/  ch ) ).
16 pm1.4 375 . . . . 5  |-  ( (
ph  \/  ch )  ->  ( ch  \/  ph ) )
1715, 16e2 28708 . . . 4  |-  (. ( ph 
<->  ps ) ,. ( ch  \/  ps )  ->.  ( ch  \/  ph ) ).
1817in2 28682 . . 3  |-  (. ( ph 
<->  ps )  ->.  ( ( ch  \/  ps )  -> 
( ch  \/  ph ) ) ).
19 bi3 179 . . 3  |-  ( ( ( ch  \/  ph )  ->  ( ch  \/  ps ) )  ->  (
( ( ch  \/  ps )  ->  ( ch  \/  ph ) )  ->  ( ( ch  \/  ph )  <->  ( ch  \/  ps ) ) ) )
2010, 18, 19e11 28765 . 2  |-  (. ( ph 
<->  ps )  ->.  ( ( ch  \/  ph )  <->  ( ch  \/  ps ) ) ).
2120in1 28638 1  |-  ( (
ph 
<->  ps )  ->  (
( ch  \/  ph ) 
<->  ( ch  \/  ps ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    \/ wo 357
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-vd1 28637  df-vd2 28646
  Copyright terms: Public domain W3C validator