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

Theorem exbiriVD 34054
Description: Virtual deduction proof of exbiri 620. 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.
h1::  |-  ( ( ph  /\  ps )  ->  ( ch  <->  th ) )
2::  |-  (. ph  ->.  ph ).
3::  |-  (. ph ,. ps  ->.  ps ).
4::  |-  (. ph ,. ps ,. th  ->.  th ).
5:2,1,?: e10 33874  |-  (. ph  ->.  ( ps  ->  ( ch  <->  th ) ) ).
6:3,5,?: e21 33921  |-  (. ph ,. ps  ->.  ( ch  <->  th ) ).
7:4,6,?: e32 33949  |-  (. ph ,. ps ,. th  ->.  ch ).
8:7:  |-  (. ph ,. ps  ->.  ( th  ->  ch ) ).
9:8:  |-  (. ph  ->.  ( ps  ->  ( th  ->  ch ) ) ).
qed:9:  |-  ( ph  ->  ( ps  ->  ( th  ->  ch ) ) )
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypothesis
Ref Expression
exbiriVD.1  |-  ( (
ph  /\  ps )  ->  ( ch  <->  th )
)
Assertion
Ref Expression
exbiriVD  |-  ( ph  ->  ( ps  ->  ( th  ->  ch ) ) )

Proof of Theorem exbiriVD
StepHypRef Expression
1 idn3 33795 . . . . 5  |-  (. ph ,. ps ,. th  ->.  th ).
2 idn2 33793 . . . . . 6  |-  (. ph ,. ps  ->.  ps ).
3 idn1 33745 . . . . . . 7  |-  (. ph  ->.  ph ).
4 exbiriVD.1 . . . . . . 7  |-  ( (
ph  /\  ps )  ->  ( ch  <->  th )
)
5 pm3.3 442 . . . . . . . 8  |-  ( ( ( ph  /\  ps )  ->  ( ch  <->  th )
)  ->  ( ph  ->  ( ps  ->  ( ch 
<->  th ) ) ) )
65com12 31 . . . . . . 7  |-  ( ph  ->  ( ( ( ph  /\ 
ps )  ->  ( ch 
<->  th ) )  -> 
( ps  ->  ( ch 
<->  th ) ) ) )
73, 4, 6e10 33874 . . . . . 6  |-  (. ph  ->.  ( ps  ->  ( ch  <->  th ) ) ).
8 pm2.27 39 . . . . . 6  |-  ( ps 
->  ( ( ps  ->  ( ch  <->  th ) )  -> 
( ch  <->  th )
) )
92, 7, 8e21 33921 . . . . 5  |-  (. ph ,. ps  ->.  ( ch  <->  th ) ).
10 bi2 198 . . . . . 6  |-  ( ( ch  <->  th )  ->  ( th  ->  ch ) )
1110com12 31 . . . . 5  |-  ( th 
->  ( ( ch  <->  th )  ->  ch ) )
121, 9, 11e32 33949 . . . 4  |-  (. ph ,. ps ,. th  ->.  ch ).
1312in3 33789 . . 3  |-  (. ph ,. ps  ->.  ( th  ->  ch ) ).
1413in2 33785 . 2  |-  (. ph  ->.  ( ps  ->  ( th  ->  ch ) ) ).
1514in1 33742 1  |-  ( ph  ->  ( ps  ->  ( th  ->  ch ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367
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 369  df-3an 973  df-vd1 33741  df-vd2 33749  df-vd3 33761
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator