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 6	. 2 |- (ps -> ch)
5	1, 4	ax-mp 6	1 |- ch

Syntax hints:   -> wi 2

This theorem is referenced by:  pm2.61i 110  impbi 139  pm3.2i 234  jaoi 275  sstri 1512  intasym 2627  intirr 2628  fun0 2691  funopabex 2742  fvex 2838  fvsn 2879  fvresex 2909  tfrlem13 2961  tz7.44-1 2966  tz7.44-2 2967  tz7.44-3 2968  oprabex 3044  qsex 3231  undom 3342  0dom 3366  php 3409  inf0 3457  rankval3 3525  aceq3lem 3555  ac6lem 3575  numthlem 3598  zornlem1 3603  unxpdomlem 3649  cardprc 3667  cdaassen 3725  cdadom3 3729  prcdpq 3891  nthruc 4784  nthruz 4785  fac0 4871  fac1 4872  facp1t 4873  ruclem5 4889  ruc 4924  xpnnen 4927  znnen 4930  qnnen 4931  infxpidmlem1 4933  infxpidmlem11 4943  infxpidmlem12 4944  infunabs 4946  infdif 4948  infmap2 4953  hlimunii 5143  hosmvalt 5487  hodmvalt 5488  pjnorm 5663

This theorem was proved from axioms:  ax-mp 6

metamath.org