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

Theorem exbirVD 28629
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 28499  |-  (. ( ( ph  /\  ps )  ->  ( ch  <->  th ) ) ,  ( ph  /\  ps )  ->.  ( ch  <->  th ) ).
6:3,5,?: e32 28533  |-  (. ( ( 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_ 28399  |-  (. ( ( 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 28387 . . . . . 6  |-  (. (
( ph  /\  ps )  ->  ( ch  <->  th )
) ,. ( ph  /\ 
ps ) ,. th  ->.  th
).
2 idn1 28342 . . . . . . 7  |-  (. (
( ph  /\  ps )  ->  ( ch  <->  th )
) 
->.  ( ( ph  /\  ps )  ->  ( ch  <->  th ) ) ).
3 idn2 28385 . . . . . . 7  |-  (. (
( ph  /\  ps )  ->  ( ch  <->  th )
) ,. ( ph  /\ 
ps )  ->.  ( ph  /\ 
ps ) ).
4 id 19 . . . . . . 7  |-  ( ( ( ph  /\  ps )  ->  ( ch  <->  th )
)  ->  ( ( ph  /\  ps )  -> 
( ch  <->  th )
) )
52, 3, 4e12 28499 . . . . . 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 28533 . . . . 5  |-  (. (
( ph  /\  ps )  ->  ( ch  <->  th )
) ,. ( ph  /\ 
ps ) ,. th  ->.  ch
).
98in3 28381 . . . 4  |-  (. (
( ph  /\  ps )  ->  ( ch  <->  th )
) ,. ( ph  /\ 
ps )  ->.  ( th  ->  ch ) ).
109in2 28377 . . 3  |-  (. (
( ph  /\  ps )  ->  ( ch  <->  th )
) 
->.  ( ( ph  /\  ps )  ->  ( th 
->  ch ) ) ).
11 pm3.3 431 . . 3  |-  ( ( ( ph  /\  ps )  ->  ( th  ->  ch ) )  ->  ( ph  ->  ( ps  ->  ( th  ->  ch )
) ) )
1210, 11e1_ 28399 . 2  |-  (. (
( ph  /\  ps )  ->  ( ch  <->  th )
) 
->.  ( ph  ->  ( ps  ->  ( th  ->  ch ) ) ) ).
1312in1 28339 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 28338  df-vd2 28347  df-vd3 28359
  Copyright terms: Public domain W3C validator