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 2044  intab 2528  intasym 3389  intirr 3390  fun0 3485  fvsn 3733  tfrlem13 3862  tz7.44-1 3867  tz7.44-2 3868  undom 4372  0dom 4398  php 4445  pwfilem 4496  inf0 4530  rankval3 4605  brdom3 4725  brdom5 4726  brdom4 4727  unxpdomlem 4766  cardprc 4784  cdaassen 4853  cdadom3 4858  prcdpq 5020  nthruc 6627  nthruz 6628  caubnd 6814  climubi 7040  caucvg3lem 7053  dsupivthlem 7177  ivth2OLD 7185  eirrlem2 7282  eirrlem5 7285  xpnnen 7392  znnen 7396  qnnen 7397  ruc 7443  infxpidmlem1 7446  infxpidmlem11 7456  infxpidmlem12 7457  infunabs 7459  infdif 7462  infdif2 7463  infmap2 7474  ghgrpilem4 8021  phrel 8340  bnrel 8393  hlrel 8460  cmpfun 8722  hlimunii 9259  pjnorm 9797  lnopunilem1 10064  lnophmlem1 10070

This theorem was proved from axioms:  ax-mp 7

Copyright terms: Public domain