Metamath Proof Explorer

Theorem adh-minim-ax2c

Description: Derivation of a commuted form of ax-2 from adh-minim and ax-mp . Polish prefix notation: CCpqCCpCqrCpr . (Contributed by ADH, 10-Nov-2023) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion adh-minim-ax2c 
|- ( ( ph -> ps ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) )

Proof

Step Hyp Ref Expression
1 adh-minim-ax2-lem5 
 |-  ( ( ph -> ps ) -> ( ( ( ( ( ( th -> ta ) -> et ) -> ( ( ta -> ( et -> ze ) ) -> ( ta -> ze ) ) ) -> ph ) -> ps ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) )
2 adh-minim-ax2-lem6 
 |-  ( ( ( ( ( si -> rh ) -> mu ) -> ( ( rh -> ( mu -> la ) ) -> ( rh -> la ) ) ) -> ( ( ( ( th -> ta ) -> et ) -> ( ( ta -> ( et -> ze ) ) -> ( ta -> ze ) ) ) -> ph ) ) -> ( ( ( ( si -> rh ) -> mu ) -> ( ( rh -> ( mu -> la ) ) -> ( rh -> la ) ) ) -> ph ) )
3 adh-minim-ax2-lem6 
 |-  ( ( ( ( ( ( si -> rh ) -> mu ) -> ( ( rh -> ( mu -> la ) ) -> ( rh -> la ) ) ) -> ( ( ( ( th -> ta ) -> et ) -> ( ( ta -> ( et -> ze ) ) -> ( ta -> ze ) ) ) -> ph ) ) -> ( ( ( ( si -> rh ) -> mu ) -> ( ( rh -> ( mu -> la ) ) -> ( rh -> la ) ) ) -> ph ) ) -> ( ( ( ( ( si -> rh ) -> mu ) -> ( ( rh -> ( mu -> la ) ) -> ( rh -> la ) ) ) -> ( ( ( ( th -> ta ) -> et ) -> ( ( ta -> ( et -> ze ) ) -> ( ta -> ze ) ) ) -> ph ) ) -> ph ) )
4 2 3 ax-mp 
 |-  ( ( ( ( ( si -> rh ) -> mu ) -> ( ( rh -> ( mu -> la ) ) -> ( rh -> la ) ) ) -> ( ( ( ( th -> ta ) -> et ) -> ( ( ta -> ( et -> ze ) ) -> ( ta -> ze ) ) ) -> ph ) ) -> ph )
5 adh-minim-ax1-ax2-lem4 
 |-  ( ( ( ( ( ( si -> rh ) -> mu ) -> ( ( rh -> ( mu -> la ) ) -> ( rh -> la ) ) ) -> ( ( ( ( th -> ta ) -> et ) -> ( ( ta -> ( et -> ze ) ) -> ( ta -> ze ) ) ) -> ph ) ) -> ph ) -> ( ( ( ( ( ( th -> ta ) -> et ) -> ( ( ta -> ( et -> ze ) ) -> ( ta -> ze ) ) ) -> ph ) -> ( ph -> ps ) ) -> ( ( ( ( ( th -> ta ) -> et ) -> ( ( ta -> ( et -> ze ) ) -> ( ta -> ze ) ) ) -> ph ) -> ps ) ) )
6 4 5 ax-mp 
 |-  ( ( ( ( ( ( th -> ta ) -> et ) -> ( ( ta -> ( et -> ze ) ) -> ( ta -> ze ) ) ) -> ph ) -> ( ph -> ps ) ) -> ( ( ( ( ( th -> ta ) -> et ) -> ( ( ta -> ( et -> ze ) ) -> ( ta -> ze ) ) ) -> ph ) -> ps ) )
7 adh-minim-ax1-ax2-lem4 
 |-  ( ( ( ( ( ( ( th -> ta ) -> et ) -> ( ( ta -> ( et -> ze ) ) -> ( ta -> ze ) ) ) -> ph ) -> ( ph -> ps ) ) -> ( ( ( ( ( th -> ta ) -> et ) -> ( ( ta -> ( et -> ze ) ) -> ( ta -> ze ) ) ) -> ph ) -> ps ) ) -> ( ( ( ph -> ps ) -> ( ( ( ( ( ( th -> ta ) -> et ) -> ( ( ta -> ( et -> ze ) ) -> ( ta -> ze ) ) ) -> ph ) -> ps ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) -> ( ( ph -> ps ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) )
8 6 7 ax-mp 
 |-  ( ( ( ph -> ps ) -> ( ( ( ( ( ( th -> ta ) -> et ) -> ( ( ta -> ( et -> ze ) ) -> ( ta -> ze ) ) ) -> ph ) -> ps ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) ) -> ( ( ph -> ps ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) ) )
9 1 8 ax-mp 
 |-  ( ( ph -> ps ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) )