Theorem mp2 54

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 139  pm2.65i 149  impbii 173  pm3.2i 305  jaoi 366  sstri 2459  intab 3069  relres 4053  intasymOLD 4118  asymrefOLD 4120  intirrOLD 4124  fun0 4283  fvsn 4569  fparlem3 4894  fparlem4 4895  tfrlem13 4942  tz7.44-1 4947  tz7.44-2 4948  undom 5308  ac6sfilem3 5319  0dom 5338  php 5417  pwfilem 5470  inf0 5521  rankval3 5601  omsublim 5683  brdom3 5759  brdom5 5760  brdom4 5761  unxpdomlem 5791  cardprc 5809  cdaassen 5876  cdadom3 5881  prcdpq 6045  cardfz 7514  nthruc 7790  nthruz 7791  caubndi 7973  faclbnd4lem1 7995  climubii 8208  caucvg3lem 8221  dsupivthlem 8348  eirrlem2 8447  eirrlem5 8450  xpnnen 8563  znnen 8566  qnnen 8567  ruc 8613  infxpidmlem1 8616  infxpidmlem11 8626  infxpidmlem12 8627  infunabs 8629  infdif 8632  infdif2 8633  infmap2 8645  ghgrpilem4 9239  phrel 9610  bnrel 9664  hlrel 9734  limfil 10089  isfilmap 10100  sflimf 10110  hlimuniii 10533  pjnormi 11093  lnopunilem1 11364  lnophmlem1 11370  bnj1024 12671  mulgcdlem5 13552  naim1i 13866  naim2i 13867  mont 13889  sqpeq 14106  cmpfun 14207  nZdef 14253  domrancur1c 14276  dfps2 14359  seqzp2 14439  rcfpfillem3 14644  rcfpfillem5 14646  limvinlv 14655  invtrgrp 14693  cntrsetlem 14709  omsublimOLD 15078  2ndc1stc 15159  2ndcctbss 15160  neibastop2lem4 15204  sfcls 15286  filclus 15287  sfclusf 15306  tailf 15315  istail 15316  incsequz2 15498  txmet 15607  totbndbnd 15626  phtpycom 15732  ltfrn 16120  e000 16293  e00 16294

This theorem was proved from axioms:  ax-mp 7

Copyright terms: Public domain