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

Theorem simplbi2comgVD 29098
Description: Virtual deduction proof of simplbi2comg 1383. 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 1383 is simplbi2comgVD 29098 without virtual deductions and was automatically derived from simplbi2comgVD 29098.
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 28763 . . . . 5  |-  (. ( ph 
<->  ( ps  /\  ch ) )  ->.  ( ph  <->  ( ps  /\  ch )
) ).
2 bi2 191 . . . . 5  |-  ( (
ph 
<->  ( ps  /\  ch ) )  ->  (
( ps  /\  ch )  ->  ph ) )
31, 2e1_ 28826 . . . 4  |-  (. ( ph 
<->  ( ps  /\  ch ) )  ->.  ( ( ps  /\  ch )  ->  ph ) ).
4 pm3.3 433 . . . 4  |-  ( ( ( ps  /\  ch )  ->  ph )  ->  ( ps  ->  ( ch  ->  ph ) ) )
53, 4e1_ 28826 . . 3  |-  (. ( ph 
<->  ( ps  /\  ch ) )  ->.  ( ps  ->  ( ch  ->  ph )
) ).
6 pm2.04 79 . . 3  |-  ( ( ps  ->  ( ch  ->  ph ) )  -> 
( ch  ->  ( ps  ->  ph ) ) )
75, 6e1_ 28826 . 2  |-  (. ( ph 
<->  ( ps  /\  ch ) )  ->.  ( ch  ->  ( ps  ->  ph )
) ).
87in1 28760 1  |-  ( (
ph 
<->  ( ps  /\  ch ) )  ->  ( ch  ->  ( ps  ->  ph ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360
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 179  df-an 362  df-vd1 28759
  Copyright terms: Public domain W3C validator