Theorem frege36 38133

Description: The case in which ps is denied, -. ph is affirmed, and ph is affirmed does not occur. If ph occurs, then (at least) one of the two, ph or ps, takes place (no matter what ps might be). Identical to pm2.24 121. Proposition 36 of [Frege1879] p. 45. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)

Assertion

Ref	Expression
frege36	|- ( ph -> ( -. ph -> ps ) )

Proof of Theorem frege36

Step	Hyp	Ref	Expression
1		ax-frege1 38084	. 2 |- ( ph -> ( -. ps -> ph ) )
2		frege34 38131	. 2 |- ( ( ph -> ( -. ps -> ph ) ) -> ( ph -> ( -. ph -> ps ) ) )
3	1, 2	ax-mp 5	1 |- ( ph -> ( -. ph -> ps ) )

Syntax hints:   -. wn 3   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-frege1 38084  ax-frege2 38085  ax-frege28 38124  ax-frege31 38128

This theorem is referenced by:  frege37  38134  frege38  38135  frege83  38240