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

Metamath Proof Explorer

Theorem uun0.1

Description: Convention notation form of un0.1 . (Contributed by Alan Sare, 23-Apr-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses uun0.1.1 
|- ( T. -> ph )
uun0.1.2 
|- ( ps -> ch )
uun0.1.3 
|- ( ( T. /\ ps ) -> th )
Assertion uun0.1 
|- ( ps -> th )

Proof

Step Hyp Ref Expression
1 uun0.1.1 
 |-  ( T. -> ph )
2 uun0.1.2 
 |-  ( ps -> ch )
3 uun0.1.3 
 |-  ( ( T. /\ ps ) -> th )
4 tru 
 |-  T.
5 1 2 pm3.2i 
 |-  ( ( T. -> ph ) /\ ( ps -> ch ) )
6 5 3 pm3.2i 
 |-  ( ( ( T. -> ph ) /\ ( ps -> ch ) ) /\ ( ( T. /\ ps ) -> th ) )
7 6 simpri 
 |-  ( ( T. /\ ps ) -> th )
8 7 ex 
 |-  ( T. -> ( ps -> th ) )
9 4 8 ax-mp 
 |-  ( ps -> th )