Theorem mp2 43

Description: A double modus ponens inference.

Hypotheses

Ref	Expression
mp2.1	|- ph
mp2.2	|- ps
mp2.3	|- (ph -> (ps -> ch))

Assertion

Ref	Expression
mp2	|- ch

Proof of Theorem mp2

Step	Hyp	Ref	Expression
1		mp2.2	. 2 |- ps
2		mp2.1	. . 3 |- ph
3		mp2.3	. . 3 |- (ph -> (ps -> ch))
4	2, 3	ax-mp 7	. 2 |- (ps -> ch)
5	1, 4	ax-mp 7	1 |- ch

Syntax hints:   -> wi 3

This theorem is referenced by:  pm2.61i 126  pm2.65i 135  impbi 157  pm3.2i 285  jaoi 341  sstri 2071  intab 2558  intasym 3436  asymref 3437  intirr 3439  fun0 3542  fvsn 3792  tfrlem13 3921  tz7.44-1 3926  tz7.44-2 3927  undom 4432  0dom 4458  php 4507  pwfilem 4558  inf0 4594  rankval3 4669  brdom3 4789  brdom5 4790  brdom4 4791  unxpdomlem 4831  cardprc 4849  cdaassen 4918  cdadom3 4923  prcdpq 5085  nthruc 6705  nthruz 6706  caubnd 6884  climubi 7111  caucvg3lem 7124  dsupivthlem 7249  eirrlem2 7348  eirrlem5 7351  xpnnen 7456  znnen 7459  qnnen 7460  ruc 7506  infxpidmlem1 7509  infxpidmlem11 7519  infxpidmlem12 7520  infunabs 7522  infdif 7525  infdif2 7526  infmap2 7538  ghgrpilem4 8093  phrel 8431  bnrel 8484  hlrel 8551  hlimunii 9063  pjnorm 9621  lnopunilem1 9890  lnophmlem1 9896  cmpfun 10417  rcfpfillem3 10509  rcfpfillem5 10511

This theorem was proved from axioms:  ax-mp 7

Copyright terms: Public domain