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

Theorem exbiriVD 28307
Description: Virtual deduction proof of exbiri 606. 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 28136  |-  (. ph  ->.  ( ps  ->  ( ch  <->  th ) ) ).
6:3,5,?: e21 28183  |-  (. ph ,. ps  ->.  ( ch  <->  th ) ).
7:4,6,?: e32 28211  |-  (. 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 28057 . . . . 5  |-  (. ph ,. ps ,. th  ->.  th ).
2 idn2 28055 . . . . . 6  |-  (. ph ,. ps  ->.  ps ).
3 idn1 28006 . . . . . . 7  |-  (. ph  ->.  ph ).
4 exbiriVD.1 . . . . . . 7  |-  ( (
ph  /\  ps )  ->  ( ch  <->  th )
)
5 pm3.3 432 . . . . . . . 8  |-  ( ( ( ph  /\  ps )  ->  ( ch  <->  th )
)  ->  ( ph  ->  ( ps  ->  ( ch 
<->  th ) ) ) )
65com12 29 . . . . . . 7  |-  ( ph  ->  ( ( ( ph  /\ 
ps )  ->  ( ch 
<->  th ) )  -> 
( ps  ->  ( ch 
<->  th ) ) ) )
73, 4, 6e10 28136 . . . . . 6  |-  (. ph  ->.  ( ps  ->  ( ch  <->  th ) ) ).
8 pm2.27 37 . . . . . 6  |-  ( ps 
->  ( ( ps  ->  ( ch  <->  th ) )  -> 
( ch  <->  th )
) )
92, 7, 8e21 28183 . . . . 5  |-  (. ph ,. ps  ->.  ( ch  <->  th ) ).
10 bi2 190 . . . . . 6  |-  ( ( ch  <->  th )  ->  ( th  ->  ch ) )
1110com12 29 . . . . 5  |-  ( th 
->  ( ( ch  <->  th )  ->  ch ) )
121, 9, 11e32 28211 . . . 4  |-  (. ph ,. ps ,. th  ->.  ch ).
1312in3 28051 . . 3  |-  (. ph ,. ps  ->.  ( th  ->  ch ) ).
1413in2 28047 . 2  |-  (. ph  ->.  ( ps  ->  ( th  ->  ch ) ) ).
1514in1 28003 1  |-  ( ph  ->  ( ps  ->  ( th  ->  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
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 178  df-an 361  df-3an 938  df-vd1 28002  df-vd2 28011  df-vd3 28023
  Copyright terms: Public domain W3C validator