Theorem mpdd 46

Description: A nested modus ponens deduction.

Hypotheses

Ref	Expression
mpdd.1	|- (ph -> (ps -> ch))
mpdd.2	|- (ph -> (ps -> (ch -> th)))

Assertion

Ref	Expression
mpdd	|- (ph -> (ps -> th))

Proof of Theorem mpdd

Step	Hyp	Ref	Expression
1		mpdd.1	. 2 |- (ph -> (ps -> ch))
2		mpdd.2	. . 3 |- (ph -> (ps -> (ch -> th)))
3	2	a2d 13	. 2 |- (ph -> ((ps -> ch) -> (ps -> th)))
4	1, 3	mpd 26	1 |- (ph -> (ps -> th))

Syntax hints:   -> wi 3

This theorem is referenced by:  mpid 47  mpdi 48  syldd 50  pm2.43d 65  pm2.43a 66  oaordex 4182  oaass 4185  omordi 4187  oeordsuc 4211  brecop 4296  supxrun 6040  fzoptht 6442  efifolem5 8660  nmcopexlem6 9894  nmcfnexlem6 9923  sumdmdlem 10281  mrdmcd 10602

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7

Copyright terms: Public domain