Metamath Proof Explorer


Theorem e323

Description: A virtual deduction elimination rule. (Contributed by Alan Sare, 17-Apr-2012) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 e323.1
 |-  (. ph ,. ps ,. ch ->. th ).
2 e323.2
 |-  (. ph ,. ps ->. ta ).
3 e323.3
 |-  (. ph ,. ps ,. ch ->. et ).
4 e323.4
 |-  ( th -> ( ta -> ( et -> ze ) ) )
5 1 dfvd3i
 |-  ( ph -> ( ps -> ( ch -> th ) ) )
6 2 dfvd2i
 |-  ( ph -> ( ps -> ta ) )
7 3 dfvd3i
 |-  ( ph -> ( ps -> ( ch -> et ) ) )
8 5 6 7 4 ee323
 |-  ( ph -> ( ps -> ( ch -> ze ) ) )
9 8 dfvd3ir
 |-  (. ph ,. ps ,. ch ->. ze ).