This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem e223

Description: A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Dec-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses e223.1 
|- (. ph ,. ps ->. ch ).
e223.2 
|- (. ph ,. ps ->. th ).
e223.3 
|- (. ph ,. ps ,. ta ->. et ).
e223.4 
|- ( ch -> ( th -> ( et -> ze ) ) )
Assertion e223 
|- (. ph ,. ps ,. ta ->. ze ).

Proof

Step Hyp Ref Expression
1 e223.1 
 |-  (. ph ,. ps ->. ch ).
2 e223.2 
 |-  (. ph ,. ps ->. th ).
3 e223.3 
 |-  (. ph ,. ps ,. ta ->. et ).
4 e223.4 
 |-  ( ch -> ( th -> ( et -> ze ) ) )
5 1 in2 
 |-  (. ph ->. ( ps -> ch ) ).
6 5 in1 
 |-  ( ph -> ( ps -> ch ) )
7 2 in2 
 |-  (. ph ->. ( ps -> th ) ).
8 7 in1 
 |-  ( ph -> ( ps -> th ) )
9 3 in3 
 |-  (. ph ,. ps ->. ( ta -> et ) ).
10 9 in2 
 |-  (. ph ->. ( ps -> ( ta -> et ) ) ).
11 10 in1 
 |-  ( ph -> ( ps -> ( ta -> et ) ) )
12 6 8 11 4 ee223 
 |-  ( ph -> ( ps -> ( ta -> ze ) ) )
13 12 dfvd3ir 
 |-  (. ph ,. ps ,. ta ->. ze ).