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 2076  intab 2564  intasym 3444  asymref 3445  intirr 3447  fun0 3550  fvsn 3800  tfrlem13 3929  tz7.44-1 3934  tz7.44-2 3935  undom 4444  0dom 4470  php 4519  pwfilem 4577  pwfilemOLD 4578  inf0 4615  rankval3 4691  brdom3 4811  brdom5 4812  brdom4 4813  unxpdomlem 4854  cardprc 4872  cdaassen 4942  cdadom3 4947  prcdpq 5109  nthruc 6746  nthruz 6747  caubnd 6926  faclbnd4lem1 6948  climubi 7153  caucvg3lem 7166  dsupivthlem 7291  eirrlem2 7390  eirrlem5 7393  xpnnen 7500  znnen 7503  qnnen 7504  ruc 7550  infxpidmlem1 7553  infxpidmlem11 7563  infxpidmlem12 7564  infunabs 7566  infdif 7569  infdif2 7570  infmap2 7583  ghgrpilem4 8132  phrel 8470  bnrel 8523  hlrel 8590  hlimunii 9103  pjnorm 9661  lnopunilem1 9930  lnophmlem1 9936  cmpfun 10457  rcfpfillem3 10565  rcfpfillem5 10567

This theorem was proved from axioms:  ax-mp 7

Copyright terms: Public domain