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

Theorem exbirVD 33386
Description: Virtual deduction proof of exbir 32952. 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 )  ->  ( ch  <->  th ) )  ->.  ( ( ph  /\  ps )  ->  ( ch  <->  th ) ) ).
2::  |-  (. ( ( ph  /\  ps )  ->  ( ch  <->  th ) ) ,.  ( ph  /\  ps )  ->.  ( ph  /\  ps ) ).
3::  |-  (. ( ( ph  /\  ps )  ->  ( ch  <->  th ) ) ,.  ( ph  /\  ps ) ,  th  ->.  th ).
5:1,2,?: e12 33254  |-  (. ( ( ph  /\  ps )  ->  ( ch  <->  th ) ) ,  ( ph  /\  ps )  ->.  ( ch  <->  th ) ).
6:3,5,?: e32 33288  |-  (. ( ( ph  /\  ps )  ->  ( ch  <->  th ) ) ,  ( ph  /\  ps ) ,  th  ->.  ch ).
7:6:  |-  (. ( ( ph  /\  ps )  ->  ( ch  <->  th ) ) ,  ( ph  /\  ps )  ->.  ( th  ->  ch ) ).
8:7:  |-  (. ( ( ph  /\  ps )  ->  ( ch  <->  th ) )  ->.  ( ( ph  /\  ps )  ->  ( th  ->  ch ) ) ).
9:8,?: e1a 33146  |-  (. ( ( ph  /\  ps )  ->  ( ch  <->  th ) )  ->.  ( ph  ->  ( ps  ->  ( th  ->  ch ) ) ) ).
qed:9:  |-  ( ( ( ph  /\  ps )  ->  ( ch  <->  th ) )  ->  ( ph  ->  ( ps  ->  ( th  ->  ch ) ) ) )
(Contributed by Alan Sare, 13-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
exbirVD  |-  ( ( ( ph  /\  ps )  ->  ( ch  <->  th )
)  ->  ( ph  ->  ( ps  ->  ( th  ->  ch ) ) ) )

Proof of Theorem exbirVD
StepHypRef Expression
1 idn3 33134 . . . . . 6  |-  (. (
( ph  /\  ps )  ->  ( ch  <->  th )
) ,. ( ph  /\ 
ps ) ,. th  ->.  th
).
2 idn1 33084 . . . . . . 7  |-  (. (
( ph  /\  ps )  ->  ( ch  <->  th )
) 
->.  ( ( ph  /\  ps )  ->  ( ch  <->  th ) ) ).
3 idn2 33132 . . . . . . 7  |-  (. (
( ph  /\  ps )  ->  ( ch  <->  th )
) ,. ( ph  /\ 
ps )  ->.  ( ph  /\ 
ps ) ).
4 id 22 . . . . . . 7  |-  ( ( ( ph  /\  ps )  ->  ( ch  <->  th )
)  ->  ( ( ph  /\  ps )  -> 
( ch  <->  th )
) )
52, 3, 4e12 33254 . . . . . 6  |-  (. (
( ph  /\  ps )  ->  ( ch  <->  th )
) ,. ( ph  /\ 
ps )  ->.  ( ch  <->  th ) ).
6 bi2 198 . . . . . . 7  |-  ( ( ch  <->  th )  ->  ( th  ->  ch ) )
76com12 31 . . . . . 6  |-  ( th 
->  ( ( ch  <->  th )  ->  ch ) )
81, 5, 7e32 33288 . . . . 5  |-  (. (
( ph  /\  ps )  ->  ( ch  <->  th )
) ,. ( ph  /\ 
ps ) ,. th  ->.  ch
).
98in3 33128 . . . 4  |-  (. (
( ph  /\  ps )  ->  ( ch  <->  th )
) ,. ( ph  /\ 
ps )  ->.  ( th  ->  ch ) ).
109in2 33124 . . 3  |-  (. (
( ph  /\  ps )  ->  ( ch  <->  th )
) 
->.  ( ( ph  /\  ps )  ->  ( th 
->  ch ) ) ).
11 pm3.3 444 . . 3  |-  ( ( ( ph  /\  ps )  ->  ( th  ->  ch ) )  ->  ( ph  ->  ( ps  ->  ( th  ->  ch )
) ) )
1210, 11e1a 33146 . 2  |-  (. (
( ph  /\  ps )  ->  ( ch  <->  th )
) 
->.  ( ph  ->  ( ps  ->  ( th  ->  ch ) ) ) ).
1312in1 33081 1  |-  ( ( ( ph  /\  ps )  ->  ( ch  <->  th )
)  ->  ( ph  ->  ( ps  ->  ( th  ->  ch ) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369
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-an 371  df-3an 976  df-vd1 33080  df-vd2 33088  df-vd3 33100
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator