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

Theorem exbiriVD 28630
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 28467  |-  (. ph  ->.  ( ps  ->  ( ch  <->  th ) ) ).
6:3,5,?: e21 28505  |-  (. ph ,. ps  ->.  ( ch  <->  th ) ).
7:4,6,?: e32 28533  |-  (. 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 28387 . . . . 5  |-  (. ph ,. ps ,. th  ->.  th ).
2 idn2 28385 . . . . . 6  |-  (. ph ,. ps  ->.  ps ).
3 idn1 28342 . . . . . . 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 28467 . . . . . 6  |-  (. ph  ->.  ( ps  ->  ( ch  <->  th ) ) ).
8 pm2.27 35 . . . . . 6  |-  ( ps 
->  ( ( ps  ->  ( ch  <->  th ) )  -> 
( ch  <->  th )
) )
92, 7, 8e21 28505 . . . . 5  |-  (. ph ,. ps  ->.  ( ch  <->  th ) ).
10 bi2 189 . . . . . 6  |-  ( ( ch  <->  th )  ->  ( th  ->  ch ) )
1110com12 27 . . . . 5  |-  ( th 
->  ( ( ch  <->  th )  ->  ch ) )
121, 9, 11e32 28533 . . . 4  |-  (. ph ,. ps ,. th  ->.  ch ).
1312in3 28381 . . 3  |-  (. ph ,. ps  ->.  ( th  ->  ch ) ).
1413in2 28377 . 2  |-  (. ph  ->.  ( ps  ->  ( th  ->  ch ) ) ).
1514in1 28339 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 28338  df-vd2 28347  df-vd3 28359
  Copyright terms: Public domain W3C validator