![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mp2 | GIF version |
Description: A double modus ponens inference. (Contributed by NM, 5-Apr-1994.) (Proof shortened by Wolf Lammen, 23-Jul-2013.) |
Ref | Expression |
---|---|
mp2.1 | ⊢ 𝜑 |
mp2.2 | ⊢ 𝜓 |
mp2.3 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
mp2 | ⊢ 𝜒 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mp2.1 | . 2 ⊢ 𝜑 | |
2 | mp2.2 | . . 3 ⊢ 𝜓 | |
3 | mp2.3 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
4 | 2, 3 | mpi 15 | . 2 ⊢ (𝜑 → 𝜒) |
5 | 1, 4 | ax-mp 5 | 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: impbii 125 pm3.2i 270 sstri 3111 0disj 3934 disjx0 3936 ontr2exmid 4448 0elsucexmid 4488 relres 4855 cnvdif 4953 funopab4 5168 fun0 5189 fvsn 5623 reltpos 6155 tpostpos 6169 tpos0 6179 oawordriexmid 6374 swoer 6465 xpider 6508 erinxp 6511 domfiexmid 6780 diffitest 6789 ltrel 7850 lerel 7852 frecfzennn 10230 sum0 11189 qnnen 11980 pw1dom2 13361 |
Copyright terms: Public domain | W3C validator |