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 3076 0disj 3896 disjx0 3898 ontr2exmid 4410 0elsucexmid 4450 relres 4817 cnvdif 4915 funopab4 5130 fun0 5151 fvsn 5583 reltpos 6115 tpostpos 6129 tpos0 6139 oawordriexmid 6334 swoer 6425 xpider 6468 erinxp 6471 domfiexmid 6740 diffitest 6749 ltrel 7794 lerel 7796 frecfzennn 10167 sum0 11125 qnnen 11871 pw1dom2 13117 |
Copyright terms: Public domain | W3C validator |