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

Theorem exbirVD 28945
Description: Virtual deduction proof of exbir 1355. 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 28813  |-  (. ( ( ph  /\  ps )  ->  ( ch  <->  th ) ) ,  ( ph  /\  ps )  ->.  ( ch  <->  th ) ).
6:3,5,?: e32 28847  |-  (. ( ( 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,?: e1_ 28704  |-  (. ( ( 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 28692 . . . . . 6  |-  (. (
( ph  /\  ps )  ->  ( ch  <->  th )
) ,. ( ph  /\ 
ps ) ,. th  ->.  th
).
2 idn1 28641 . . . . . . 7  |-  (. (
( ph  /\  ps )  ->  ( ch  <->  th )
) 
->.  ( ( ph  /\  ps )  ->  ( ch  <->  th ) ) ).
3 idn2 28690 . . . . . . 7  |-  (. (
( ph  /\  ps )  ->  ( ch  <->  th )
) ,. ( ph  /\ 
ps )  ->.  ( ph  /\ 
ps ) ).
4 id 19 . . . . . . 7  |-  ( ( ( ph  /\  ps )  ->  ( ch  <->  th )
)  ->  ( ( ph  /\  ps )  -> 
( ch  <->  th )
) )
52, 3, 4e12 28813 . . . . . 6  |-  (. (
( ph  /\  ps )  ->  ( ch  <->  th )
) ,. ( ph  /\ 
ps )  ->.  ( ch  <->  th ) ).
6 bi2 189 . . . . . . 7  |-  ( ( ch  <->  th )  ->  ( th  ->  ch ) )
76com12 27 . . . . . 6  |-  ( th 
->  ( ( ch  <->  th )  ->  ch ) )
81, 5, 7e32 28847 . . . . 5  |-  (. (
( ph  /\  ps )  ->  ( ch  <->  th )
) ,. ( ph  /\ 
ps ) ,. th  ->.  ch
).
98in3 28686 . . . 4  |-  (. (
( ph  /\  ps )  ->  ( ch  <->  th )
) ,. ( ph  /\ 
ps )  ->.  ( th  ->  ch ) ).
109in2 28682 . . 3  |-  (. (
( ph  /\  ps )  ->  ( ch  <->  th )
) 
->.  ( ( ph  /\  ps )  ->  ( th 
->  ch ) ) ).
11 pm3.3 431 . . 3  |-  ( ( ( ph  /\  ps )  ->  ( th  ->  ch ) )  ->  ( ph  ->  ( ps  ->  ( th  ->  ch )
) ) )
1210, 11e1_ 28704 . 2  |-  (. (
( ph  /\  ps )  ->  ( ch  <->  th )
) 
->.  ( ph  ->  ( ps  ->  ( th  ->  ch ) ) ) ).
1312in1 28638 1  |-  ( ( ( ph  /\  ps )  ->  ( ch  <->  th )
)  ->  ( ph  ->  ( ps  ->  ( th  ->  ch ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
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-an 360  df-3an 936  df-vd1 28637  df-vd2 28646  df-vd3 28658
  Copyright terms: Public domain W3C validator