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 700  reuuniss2 2881  peano5 3143  oeordi 4198  prlem936 5127  negeu 5327  receu 5670  caubnd 6863  clm4le 7019  climaddlem3 7052  climmullem8 7063  climcau 7092  caucvglem2 7094  cvgratlem1ALT 7182  cvgratlem1 7185  cvgratlem4 7188  uniopnt 7540  islp2 7688  metxplem4 7773  lmle 7895  metelcls 7900  metcnp4 7904  grpid 7999  blocnilem 8395  minveclem27 8502  nmcopexlem6 9871  nmcfnexlem6 9900  hmopidmch 9990  dmdbr3 10141  dmdbr4 10142  atom1d 10188  infi1 10347  fiiu 10350  fiiu2 10377  hmeogrp 10425  cnfilca 10451

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

Copyright terms: Public domain