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

Theorem simplbi2comgVD 28426
Description: Virtual deduction proof of simplbi2comg 1373. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. simplbi2comg 1373 is simplbi2comgVD 28426 without virtual deductions and was automatically derived from simplbi2comgVD 28426.
1::  |-  (. ( ph  <->  ( ps  /\  ch ) )  ->.  ( ph  <->  (  ps  /\  ch ) ) ).
2:1:  |-  (. ( ph  <->  ( ps  /\  ch ) )  ->.  ( ( ps  /\  ch  )  ->  ph ) ).
3:2:  |-  (. ( ph  <->  ( ps  /\  ch ) )  ->.  ( ps  ->  ( ch  ->  ph ) ) ).
4:3:  |-  (. ( ph  <->  ( ps  /\  ch ) )  ->.  ( ch  ->  ( ps  ->  ph ) ) ).
qed:4:  |-  ( ( ph  <->  ( ps  /\  ch ) )  ->  ( ch  ->  ( ps  ->  ph ) ) )
(Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
simplbi2comgVD  |-  ( (
ph 
<->  ( ps  /\  ch ) )  ->  ( ch  ->  ( ps  ->  ph ) ) )

Proof of Theorem simplbi2comgVD
StepHypRef Expression
1 idn1 28087 . . . . 5  |-  (. ( ph 
<->  ( ps  /\  ch ) )  ->.  ( ph  <->  ( ps  /\  ch )
) ).
2 bi2 189 . . . . 5  |-  ( (
ph 
<->  ( ps  /\  ch ) )  ->  (
( ps  /\  ch )  ->  ph ) )
31, 2e1_ 28150 . . . 4  |-  (. ( ph 
<->  ( ps  /\  ch ) )  ->.  ( ( ps  /\  ch )  ->  ph ) ).
4 pm3.3 431 . . . 4  |-  ( ( ( ps  /\  ch )  ->  ph )  ->  ( ps  ->  ( ch  ->  ph ) ) )
53, 4e1_ 28150 . . 3  |-  (. ( ph 
<->  ( ps  /\  ch ) )  ->.  ( ps  ->  ( ch  ->  ph )
) ).
6 pm2.04 76 . . 3  |-  ( ( ps  ->  ( ch  ->  ph ) )  -> 
( ch  ->  ( ps  ->  ph ) ) )
75, 6e1_ 28150 . 2  |-  (. ( ph 
<->  ( ps  /\  ch ) )  ->.  ( ch  ->  ( ps  ->  ph )
) ).
87in1 28084 1  |-  ( (
ph 
<->  ( ps  /\  ch ) )  ->  ( ch  ->  ( ps  ->  ph ) ) )
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-vd1 28083
  Copyright terms: Public domain W3C validator