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

Theorem exbiriVD 28946
Description: Virtual deduction proof of exbiri 605. 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 28772  |-  (. ph  ->.  ( ps  ->  ( ch  <->  th ) ) ).
6:3,5,?: e21 28819  |-  (. ph ,. ps  ->.  ( ch  <->  th ) ).
7:4,6,?: e32 28847  |-  (. 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 28692 . . . . 5  |-  (. ph ,. ps ,. th  ->.  th ).
2 idn2 28690 . . . . . 6  |-  (. ph ,. ps  ->.  ps ).
3 idn1 28641 . . . . . . 7  |-  (. ph  ->.  ph ).
4 exbiriVD.1 . . . . . . 7  |-  ( (
ph  /\  ps )  ->  ( ch  <->  th )
)
5 pm3.3 431 . . . . . . . 8  |-  ( ( ( ph  /\  ps )  ->  ( ch  <->  th )
)  ->  ( ph  ->  ( ps  ->  ( ch 
<->  th ) ) ) )
65com12 27 . . . . . . 7  |-  ( ph  ->  ( ( ( ph  /\ 
ps )  ->  ( ch 
<->  th ) )  -> 
( ps  ->  ( ch 
<->  th ) ) ) )
73, 4, 6e10 28772 . . . . . 6  |-  (. ph  ->.  ( ps  ->  ( ch  <->  th ) ) ).
8 pm2.27 35 . . . . . 6  |-  ( ps 
->  ( ( ps  ->  ( ch  <->  th ) )  -> 
( ch  <->  th )
) )
92, 7, 8e21 28819 . . . . 5  |-  (. ph ,. ps  ->.  ( ch  <->  th ) ).
10 bi2 189 . . . . . 6  |-  ( ( ch  <->  th )  ->  ( th  ->  ch ) )
1110com12 27 . . . . 5  |-  ( th 
->  ( ( ch  <->  th )  ->  ch ) )
121, 9, 11e32 28847 . . . 4  |-  (. ph ,. ps ,. th  ->.  ch ).
1312in3 28686 . . 3  |-  (. ph ,. ps  ->.  ( th  ->  ch ) ).
1413in2 28682 . 2  |-  (. ph  ->.  ( ps  ->  ( th  ->  ch ) ) ).
1514in1 28638 1  |-  ( 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