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 4192  oaass 4195  omordi 4197  oeordsuc 4221  brecop 4306  supxrun 6085  fzoptht 6502  spwpr3OLD 8662  efifolem5 8726  nmcopexlem6 9956  nmcfnexlem6 9985  sumdmdlem 10345  mrdmcd 10722

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

Copyright terms: Public domain