Metamath Proof Explorer

Theorem simplbi2VD

Description: Virtual deduction proof of simplbi2 . 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 ) )
3:1,?: e0a |- ( ( ps /\ ch ) -> ph )
qed:3,?: e0a |- ( ps -> ( ch -> ph ) )
The proof of simplbi2 was automatically derived from it. (Contributed by Alan Sare, 31-Dec-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis pm3.26bi2VD.1 
|- ( ph <-> ( ps /\ ch ) )
Assertion simplbi2VD 
|- ( ps -> ( ch -> ph ) )

Proof

Step Hyp Ref Expression
1 pm3.26bi2VD.1 
 |-  ( ph <-> ( ps /\ ch ) )
2 biimpr 
 |-  ( ( ph <-> ( ps /\ ch ) ) -> ( ( ps /\ ch ) -> ph ) )
3 1 2 e0a 
 |-  ( ( ps /\ ch ) -> ph )
4 pm3.3 
 |-  ( ( ( ps /\ ch ) -> ph ) -> ( ps -> ( ch -> ph ) ) )
5 3 4 e0a 
 |-  ( ps -> ( ch -> ph ) )