Theorem mp2 43

Description: A double modus ponens inference.

Hypotheses

Ref	Expression
mp2.1	⊢ φ
mp2.2	⊢ ψ
mp2.3	⊢ (φ → (ψ → χ))

Assertion

Ref	Expression
mp2	⊢ χ

Proof of Theorem mp2

Step	Hyp	Ref	Expression
1		mp2.2	. 2 ⊢ ψ
2		mp2.1	. . 3 ⊢ φ
3		mp2.3	. . 3 ⊢ (φ → (ψ → χ))
4	2, 3	ax-mp 7	. 2 ⊢ (ψ → χ)
5	1, 4	ax-mp 7	1 ⊢ χ

Syntax hints:   → wi 3

This theorem is referenced by:  pm2.61i 126  pm2.65i 135  impbi 157  pm3.2i 285  jaoi 341  sstri 2069  intab 2555  intasym 3430  asymref 3431  intirr 3433  fun0 3536  fvsn 3785  tfrlem13 3914  tz7.44-1 3919  tz7.44-2 3920  undom 4424  0dom 4450  php 4499  pwfilem 4550  inf0 4586  rankval3 4661  brdom3 4781  brdom5 4782  brdom4 4783  unxpdomlem 4823  cardprc 4841  cdaassen 4910  cdadom3 4915  prcdpq 5077  nthruc 6684  nthruz 6685  caubnd 6871  climubi 7097  caucvg3lem 7110  dsupivthlem 7234  ivth2OLD 7242  eirrlem2 7339  eirrlem5 7342  xpnnen 7449  znnen 7453  qnnen 7454  ruc 7500  infxpidmlem1 7503  infxpidmlem11 7513  infxpidmlem12 7514  infunabs 7516  infdif 7519  infdif2 7520  infmap2 7531  ghgrpilem4 8088  phrel 8418  bnrel 8471  hlrel 8538  hlimunii 9047  pjnorm 9606  lnopunilem1 9873  lnophmlem1 9879  cmpfun 10399

This theorem was proved from axioms:  ax-mp 7

Copyright terms: Public domain