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 2063  intab 2550  intasym 3422  asymref 3423  asymrefOLD 3425  intirr 3427  fun0 3530  fvsn 3779  tfrlem13 3908  tz7.44-1 3913  tz7.44-2 3914  undom 4418  0dom 4444  php 4493  pwfilem 4544  inf0 4578  rankval3 4653  brdom3 4773  brdom5 4774  brdom4 4775  unxpdomlem 4815  cardprc 4833  cdaassen 4902  cdadom3 4907  prcdpq 5069  nthruc 6676  nthruz 6677  caubnd 6863  climubi 7089  caucvg3lem 7102  dsupivthlem 7226  ivth2OLD 7234  eirrlem2 7331  eirrlem5 7334  xpnnen 7441  znnen 7445  qnnen 7446  ruc 7492  infxpidmlem1 7495  infxpidmlem11 7505  infxpidmlem12 7506  infunabs 7508  infdif 7511  infdif2 7512  infmap2 7523  ghgrpilem4 8073  phrel 8405  bnrel 8458  hlrel 8525  hlimunii 9029  pjnorm 9583  lnopunilem1 9850  lnophmlem1 9856  cmpfun 10363

This theorem was proved from axioms:  ax-mp 7

Copyright terms: Public domain