Theorem pm2.27 76

Description: This theorem, called "Assertion," can be thought of as closed form of modus ponens ax-mp 7. Theorem *2.27 of [WhiteheadRussell] p. 104.

Assertion

Ref	Expression
pm2.27	|- (ph -> ((ph -> ps) -> ps))

Proof of Theorem pm2.27

Step	Hyp	Ref	Expression
1		id 73	. 2 |- ((ph -> ps) -> (ph -> ps))
2	1	com12 14	1 |- (ph -> ((ph -> ps) -> ps))

Syntax hints:   -> wi 3

This theorem is referenced by:  pm2.43 77  pm3.2im 136  mth8 137  jadOLD2 156  a1bi 213  pm3.35 384  pm2.75 631  biimt 800  meredith 1047  meredithOLD 1048  ax10o 1337  r19.27avOLD 2059  vtoclegft 2189  vtoclegftOLD 2190  el 3300  copsexg 3352  tfinds 3753  tfindsg 3755  ac6sfilem3 5319  ac6sfi 5320  ordiso 5493  xrub 7084  metequiv 8953  caun0 9018  bcthlem2 9073  vacnlem3 9464  findcard 9970  fixp 9972  fbssint 10071  fbunfip 10074  hausfillim 10095  flimopn 10113  cncomp 10123  dmdbr5 11672  waj-ax 13968  lukshef-ax2 13969  ref3w 14094  prjmapcp 14233  domrancur1c 14276  dutos1 14350  pospos 14360  tostos 14363  clfsebs 14430  fprodadd 14436  fprodneg 14464  osneisi 14596  efilcp 14636  efilcp2 14640  fbaslim2 14650  iscnp3 14660  bwt2 14674  bpmp 14933  btmp 14934  inficlALT 15054  ordisoOLD 15056  subntr 15107  compsublem 15112  compsub 15113  hscptsscld 15116  dfcon2 15124  connsub 15125  cnconn 15126  topbasfne 15181  locfincomp 15196  neibastop1 15200  isufil2 15247  fixufil 15258  limfilcf 15269  cnpfillim 15271  findcard2 15427  fimax 15428  fisupg 15430  indexfi 15437  frfi 15453  filbcmb 15458  lmtlm 15590  ax4567to6 16044  ax4567to7 16045  ax10-16 16047  smores 16128  elex22VD 16322  exbiriVD 16337

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7

Copyright terms: Public domain