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

Theorem exbiriVD 33362
Description: Virtual deduction proof of exbiri 622. 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 33188  |-  (. ph  ->.  ( ps  ->  ( ch  <->  th ) ) ).
6:3,5,?: e21 33235  |-  (. ph ,. ps  ->.  ( ch  <->  th ) ).
7:4,6,?: e32 33263  |-  (. 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 33109 . . . . 5  |-  (. ph ,. ps ,. th  ->.  th ).
2 idn2 33107 . . . . . 6  |-  (. ph ,. ps  ->.  ps ).
3 idn1 33059 . . . . . . 7  |-  (. ph  ->.  ph ).
4 exbiriVD.1 . . . . . . 7  |-  ( (
ph  /\  ps )  ->  ( ch  <->  th )
)
5 pm3.3 444 . . . . . . . 8  |-  ( ( ( ph  /\  ps )  ->  ( ch  <->  th )
)  ->  ( ph  ->  ( ps  ->  ( ch 
<->  th ) ) ) )
65com12 31 . . . . . . 7  |-  ( ph  ->  ( ( ( ph  /\ 
ps )  ->  ( ch 
<->  th ) )  -> 
( ps  ->  ( ch 
<->  th ) ) ) )
73, 4, 6e10 33188 . . . . . 6  |-  (. ph  ->.  ( ps  ->  ( ch  <->  th ) ) ).
8 pm2.27 39 . . . . . 6  |-  ( ps 
->  ( ( ps  ->  ( ch  <->  th ) )  -> 
( ch  <->  th )
) )
92, 7, 8e21 33235 . . . . 5  |-  (. ph ,. ps  ->.  ( ch  <->  th ) ).
10 bi2 198 . . . . . 6  |-  ( ( ch  <->  th )  ->  ( th  ->  ch ) )
1110com12 31 . . . . 5  |-  ( th 
->  ( ( ch  <->  th )  ->  ch ) )
121, 9, 11e32 33263 . . . 4  |-  (. ph ,. ps ,. th  ->.  ch ).
1312in3 33103 . . 3  |-  (. ph ,. ps  ->.  ( th  ->  ch ) ).
1413in2 33099 . 2  |-  (. ph  ->.  ( ps  ->  ( th  ->  ch ) ) ).
1514in1 33056 1  |-  ( 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 974  df-vd1 33055  df-vd2 33063  df-vd3 33075
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator