Metamath Proof Explorer

Theorem exbirVD

Description: Virtual deduction proof of exbir . 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.

1:: |- (. ( ( ph /\ ps ) -> ( ch <-> th ) ) ->. ( ( ph /\ ps ) -> ( ch <-> th ) ) ).
2:: |- (. ( ( ph /\ ps ) -> ( ch <-> th ) ) ,. ( ph /\ ps ) ->. ( ph /\ ps ) ).
3:: |- (. ( ( ph /\ ps ) -> ( ch <-> th ) ) ,. ( ph /\ ps ) , th ->. th ).
5:1,2,?: e12 |- (. ( ( ph /\ ps ) -> ( ch <-> th ) ) , ( ph /\ ps ) ->. ( ch <-> th ) ).
6:3,5,?: e32 |- (. ( ( ph /\ ps ) -> ( ch <-> th ) ) , ( ph /\ ps ) , th ->. ch ).
7:6: |- (. ( ( ph /\ ps ) -> ( ch <-> th ) ) , ( ph /\ ps ) ->. ( th -> ch ) ).
8:7: |- (. ( ( ph /\ ps ) -> ( ch <-> th ) ) ->. ( ( ph /\ ps ) -> ( th -> ch ) ) ).
9:8,?: e1a |- (. ( ( ph /\ ps ) -> ( ch <-> th ) ) ->. ( ph -> ( ps -> ( th -> ch ) ) ) ).
qed:9: |- ( ( ( ph /\ ps ) -> ( ch <-> th ) ) -> ( ph -> ( ps -> ( th -> ch ) ) ) )
(Contributed by Alan Sare, 13-Dec-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion exbirVD 
|- ( ( ( ph /\ ps ) -> ( ch <-> th ) ) -> ( ph -> ( ps -> ( th -> ch ) ) ) )

Proof

Step Hyp Ref Expression
1 idn3 
 |-  (. ( ( ph /\ ps ) -> ( ch <-> th ) ) ,. ( ph /\ ps ) ,. th ->. th ).
2 idn1 
 |-  (. ( ( ph /\ ps ) -> ( ch <-> th ) ) ->. ( ( ph /\ ps ) -> ( ch <-> th ) ) ).
3 idn2 
 |-  (. ( ( ph /\ ps ) -> ( ch <-> th ) ) ,. ( ph /\ ps ) ->. ( ph /\ ps ) ).
4 id 
 |-  ( ( ( ph /\ ps ) -> ( ch <-> th ) ) -> ( ( ph /\ ps ) -> ( ch <-> th ) ) )
5 2 3 4 e12 
 |-  (. ( ( ph /\ ps ) -> ( ch <-> th ) ) ,. ( ph /\ ps ) ->. ( ch <-> th ) ).
6 biimpr 
 |-  ( ( ch <-> th ) -> ( th -> ch ) )
7 6 com12 
 |-  ( th -> ( ( ch <-> th ) -> ch ) )
8 1 5 7 e32 
 |-  (. ( ( ph /\ ps ) -> ( ch <-> th ) ) ,. ( ph /\ ps ) ,. th ->. ch ).
9 8 in3 
 |-  (. ( ( ph /\ ps ) -> ( ch <-> th ) ) ,. ( ph /\ ps ) ->. ( th -> ch ) ).
10 9 in2 
 |-  (. ( ( ph /\ ps ) -> ( ch <-> th ) ) ->. ( ( ph /\ ps ) -> ( th -> ch ) ) ).
11 pm3.3 
 |-  ( ( ( ph /\ ps ) -> ( th -> ch ) ) -> ( ph -> ( ps -> ( th -> ch ) ) ) )
12 10 11 e1a 
 |-  (. ( ( ph /\ ps ) -> ( ch <-> th ) ) ->. ( ph -> ( ps -> ( th -> ch ) ) ) ).
13 12 in1 
 |-  ( ( ( ph /\ ps ) -> ( ch <-> th ) ) -> ( ph -> ( ps -> ( th -> ch ) ) ) )