![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mpi | GIF version |
Description: A nested modus ponens inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Stefan Allan, 20-Mar-2006.) |
Ref | Expression |
---|---|
mpi.1 | ⊢ 𝜓 |
mpi.2 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
mpi | ⊢ (𝜑 → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpi.1 | . . 3 ⊢ 𝜓 | |
2 | 1 | a1i 9 | . 2 ⊢ (𝜑 → 𝜓) |
3 | mpi.2 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
4 | 2, 3 | mpd 13 | 1 ⊢ (𝜑 → 𝜒) |
Colors of variables: wff set class |
Syntax hints: → wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 |
This theorem is referenced by: mp2 16 syl6mpi 64 mp2ani 432 pm2.24i 624 simplimdc 861 mp3an3 1337 3impexpbicom 1449 mpisyl 1457 equcomi 1715 equsex 1739 equsexd 1740 spimt 1747 spimeh 1750 equvini 1769 equveli 1770 sbcof2 1821 dveeq2 1826 ax11v2 1831 ax16i 1869 pm13.183 2898 euxfr2dc 2945 sbcth 2999 sbcth2 3073 ssun3 3324 ssun4 3325 ralf0 3549 exmidexmid 4225 rext 4244 exss 4256 uniopel 4285 onsucelsucexmid 4562 suc11g 4589 eunex 4593 ordsoexmid 4594 tfisi 4619 finds1 4634 omsinds 4654 relop 4812 dmrnssfld 4925 iss 4988 relcoi1 5197 nfunv 5287 funimass2 5332 fvssunirng 5569 fvmptg 5633 oprabidlem 5949 elovmpo 6117 tfrlem1 6361 oaword1 6524 0domg 6893 diffifi 6950 exmidpw 6964 djulclb 7114 0ct 7166 nlt1pig 7401 dmaddpq 7439 dmmulpq 7440 archnqq 7477 prarloclemarch2 7479 prarloclemlt 7553 cnegex 8197 nnge1 9005 zneo 9418 fsum2d 11578 fsumabs 11608 fsumiun 11620 fprod2d 11766 efne0 11821 nn0o1gt2 12046 ennnfonelemex 12571 qtopbasss 14689 ivthdichlem 14805 reeff1o 14908 coseq0negpitopi 14971 cos02pilt1 14986 logltb 15009 gausslemma2dlem0i 15173 bdop 15367 bj-nntrans 15443 |
Copyright terms: Public domain | W3C validator |