Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mp2b | GIF version |
Description: A double modus ponens inference. (Contributed by Mario Carneiro, 24-Jan-2013.) |
Ref | Expression |
---|---|
mp2b.1 | ⊢ 𝜑 |
mp2b.2 | ⊢ (𝜑 → 𝜓) |
mp2b.3 | ⊢ (𝜓 → 𝜒) |
Ref | Expression |
---|---|
mp2b | ⊢ 𝜒 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mp2b.1 | . . 3 ⊢ 𝜑 | |
2 | mp2b.2 | . . 3 ⊢ (𝜑 → 𝜓) | |
3 | 1, 2 | ax-mp 7 | . 2 ⊢ 𝜓 |
4 | mp2b.3 | . 2 ⊢ (𝜓 → 𝜒) | |
5 | 3, 4 | ax-mp 7 | 1 ⊢ 𝜒 |
Colors of variables: wff set class |
Syntax hints: → wi 4 |
This theorem was proved from axioms: ax-mp 7 |
This theorem is referenced by: eqvinc 2667 2ordpr 4249 regexmid 4260 ordsoexmid 4286 reg3exmid 4304 intasym 4709 relcoi1 4849 funres11 4971 cnvresid 4973 mpt2fvex 5829 df1st2 5840 df2nd2 5841 dftpos4 5878 tposf12 5884 xpcomco 6300 rec1nq 6493 halfnqq 6508 caucvgsrlemasr 6874 axresscn 6936 0re 7027 gtso 7097 cnegexlem2 7187 uzn0 8488 indstr 8536 dfioo2 8843 cnrecnv 9510 rexanuz 9587 climdm 9816 |
Copyright terms: Public domain | W3C validator |