Theorem mpid 47

Description: A nested modus ponens deduction.

Hypotheses

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

Assertion

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

Proof of Theorem mpid

Step	Hyp	Ref	Expression
1		mpid.1	. . 3 |- (ph -> ch)
2	1	a1d 12	. 2 |- (ph -> (ps -> ch))
3		mpid.2	. 2 |- (ph -> (ps -> (ch -> th)))
4	2, 3	mpdd 46	1 |- (ph -> (ps -> th))

Syntax hints:   -> wi 3

This theorem is referenced by:  mpan2d 701  reuuniss2 2886  peano5 3148  oeordi 4204  prlem936 5135  negeu 5335  receu 5678  caubnd 6871  clm4le 7027  climaddlem3 7060  climmullem8 7071  climcau 7100  caucvglem2 7102  cvgratlem1ALT 7190  cvgratlem1 7193  cvgratlem4 7196  uniopnt 7548  islp2 7697  metxplem4 7785  lmle 7911  metelcls 7916  metcnp4 7920  grpid 8015  blocnilem 8408  minveclem27 8515  nmcopexlem6 9894  nmcfnexlem6 9923  hmopidmch 10017  dmdbr3 10170  dmdbr4 10171  atom1d 10217  infi1 10383  fiiu 10386  fiiu2 10413  hmeogrp 10461  cnfilca 10487

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

Copyright terms: Public domain