Theorem frege34 38131

Description: If as a conseqence of the occurence of the circumstance ph, when the obstacle ps is removed, ch takes place, then from the circumstance that ch does not take place while ph occurs the occurence of the obstacle ps can be inferred. Closed form of con1d 139. Proposition 34 of [Frege1879] p. 45. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)

Assertion

Ref	Expression
frege34	|- ( ( ph -> ( -. ps -> ch ) ) -> ( ph -> ( -. ch -> ps ) ) )

Proof of Theorem frege34

Step	Hyp	Ref	Expression
1		frege33 38130	. 2 |- ( ( -. ps -> ch ) -> ( -. ch -> ps ) )
2		frege5 38094	. 2 |- ( ( ( -. ps -> ch ) -> ( -. ch -> ps ) ) -> ( ( ph -> ( -. ps -> ch ) ) -> ( ph -> ( -. ch -> ps ) ) ) )
3	1, 2	ax-mp 5	1 |- ( ( ph -> ( -. ps -> ch ) ) -> ( ph -> ( -. ch -> 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:  frege35  38132  frege36  38133