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 702  reuuniss2 2891  peano5 3153  oeordi 4214  prlem936 5155  negeu 5355  receu 5701  caubnd 6926  clm4le 7081  climaddlem3 7116  climmullem8 7127  climcau 7156  caucvglem2 7158  cvgratlem1ALT 7247  cvgratlem1 7250  cvgratlem4 7253  uniopnt 7598  islp2 7747  metxplem4 7833  lmle 7960  metelcls 7965  metcnp4 7970  grpid 8065  blocnilem 8464  minveclem27 8571  nmcopexlem6 9956  nmcfnexlem6 9985  hmopidmch 10079  dmdbr3 10232  dmdbr4 10233  atom1d 10280  infi1 10447  infi1OLD 10448  fiiu 10453  fiiuOLD 10454  fiiu2 10488  fiiu2OLD 10489  hmeogrp 10538  top2ind 10548  cnfilca 10583  cnfilcaOLD 10584

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

Copyright terms: Public domain