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 5 | . 2 ⊢ 𝜓 |
4 | mp2b.3 | . 2 ⊢ (𝜓 → 𝜒) | |
5 | 3, 4 | ax-mp 5 | 1 ⊢ 𝜒 |
Colors of variables: wff set class |
Syntax hints: → wi 4 |
This theorem was proved from axioms: ax-mp 5 |
This theorem is referenced by: eqvinc 2849 2ordpr 4501 regexmid 4512 ordsoexmid 4539 reg3exmid 4557 intasym 4988 relcoi1 5135 funres11 5260 cnvresid 5262 mpofvex 6171 df1st2 6187 df2nd2 6188 dftpos4 6231 tposf12 6237 frecabcl 6367 xp01disjl 6402 xpcomco 6792 ominf 6862 sbthlem2 6923 djuunr 7031 eldju 7033 ctssdccl 7076 ctssdclemr 7077 omct 7082 ctssexmid 7114 rec1nq 7336 halfnqq 7351 caucvgsrlemasr 7731 axresscn 7801 0re 7899 gtso 7977 cnegexlem2 8074 uzn0 9481 indstr 9531 dfioo2 9910 fnn0nninf 10372 hashinfuni 10690 hashp1i 10723 cnrecnv 10852 rexanuz 10930 xrmaxiflemcom 11190 climdm 11236 sumsnf 11350 tanvalap 11649 egt2lt3 11720 lcmgcdlem 12009 3prm 12060 sqpweven 12107 2sqpwodd 12108 qnumval 12117 qdenval 12118 xpnnen 12327 ennnfonelemhdmp1 12342 ennnfonelemss 12343 ennnfonelemnn0 12355 qnnen 12364 ctiunctal 12374 unct 12375 structcnvcnv 12410 setsslid 12444 tgrest 12809 lmbr2 12854 cnptoprest 12879 lmff 12889 tx1cn 12909 tx2cn 12910 cnblcld 13175 tgioo 13186 reeff1o 13334 pilem1 13340 efhalfpi 13360 coseq0negpitopi 13397 012of 13875 pw1nct 13883 iswomninnlem 13928 |
Copyright terms: Public domain | W3C validator |