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:  pm2.43a 66  mpan2d 706  reuuniss2 3114  peano5 3241  oeordi 4350  prlem936 5309  negeui 5509  receui 5853  caubndi 7129  clm4lei 7284  climaddlem3 7319  climmullem8 7330  climcaui 7359  caucvglem2 7361  cvgratlem1ALT 7452  cvgratlem1 7455  cvgratlem4 7458  uniopn 7810  islp2 7957  metxplem4 8043  lmle 8171  metelcls 8176  metcnp4 8181  grpid 8282  blocnilem 8719  minveclem27 8831  nmcopexlem6 10235  nmcfnexlem6 10264  hmopidmchi 10359  dmdbr3 10513  dmdbr4 10514  atom1d 10561  infi1 10735  fiiu 10738  fiiu2 10852  osneisi 11018  hmeogrp 11044  top2ind 11050  cnfilca 11088  mtord 11373  finsschain 11425  ordtypelem6 11432  omsubinit 11451  cncls 11473  cnntr 11474  uncomp 11490  hscptsscld 11491  lfinpfin 11574  comppfsc 11578  ist1-2 11603  isufil2 11650  filssufil 11656  fclusnei 11719  fcluscf 11724  flimfnfcls 11727  fcluscnplem 11729  fcluscnp 11730  fcluscomplem 11732  fcluscomp 11733  ufcomp 11734  fclusfnei 11738  filbcmb 11857  heiborlem1 12011  heiborlem28 12038

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

Copyright terms: Public domain