Theorem pm2.27 62

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	⊢ (φ → ((φ → ψ) → ψ))

Proof of Theorem pm2.27

Step	Hyp	Ref	Expression
1		id 59	. 2 ⊢ ((φ → ψ) → (φ → ψ))
2	1	com12 11	1 ⊢ (φ → ((φ → ψ) → ψ))

Syntax hints:   → wi 3

This theorem is referenced by:  pm2.43 63  pm3.2im 121  mth8 122  a1bi 195  pm3.35 357  pm2.75 577  biimt 736  meredith 931  ax10o 1176  r19.27av 1800  vtoclegft 1902  tfindsg 3213  ac6sfilem3 4590  ac6sfi 4591  xrub 6248  metequiv 8091  caun0 8156  bcthlem2 8211  vacnlem3 8584  dmdbr5 10516  ref3w 10772  pospos 10882  tostos 10883  osneisi 11018  efilcp 11083  efilcp2 11087  bwt2 11123  inficlALT 11424  ordiso 11426  subntr 11482  compsublem 11487  compsub 11488  hscptsscld 11491  cncomp 11494  dfcon2 11501  connsub 11502  cnconn 11503  topbasfne 11560  locfincomp 11575  neibastop1 11579  fbssint 11626  fbunfip 11631  isufil2 11650  fixufil 11661  flimopn 11679  limfilcf 11683  hausfillim 11685  cnpfillim 11686  morex 11804  fimax 11837  fisupg 11839  fixp 11840  indexf 11847  filbcmb 11857  lmtlm 11969

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

Copyright terms: Public domain