Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mp2b | Unicode 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 2844 2ordpr 4495 regexmid 4506 ordsoexmid 4533 reg3exmid 4551 intasym 4982 relcoi1 5129 funres11 5254 cnvresid 5256 mpofvex 6163 df1st2 6178 df2nd2 6179 dftpos4 6222 tposf12 6228 frecabcl 6358 xp01disjl 6393 xpcomco 6783 ominf 6853 sbthlem2 6914 djuunr 7022 eldju 7024 ctssdccl 7067 ctssdclemr 7068 omct 7073 ctssexmid 7105 rec1nq 7327 halfnqq 7342 caucvgsrlemasr 7722 axresscn 7792 0re 7890 gtso 7968 cnegexlem2 8065 uzn0 9472 indstr 9522 dfioo2 9901 fnn0nninf 10362 hashinfuni 10679 hashp1i 10712 cnrecnv 10838 rexanuz 10916 xrmaxiflemcom 11176 climdm 11222 sumsnf 11336 tanvalap 11635 egt2lt3 11706 lcmgcdlem 11988 3prm 12039 sqpweven 12084 2sqpwodd 12085 qnumval 12094 qdenval 12095 xpnnen 12264 ennnfonelemhdmp1 12279 ennnfonelemss 12280 ennnfonelemnn0 12292 qnnen 12301 ctiunctal 12311 unct 12312 structcnvcnv 12347 setsslid 12381 tgrest 12710 lmbr2 12755 cnptoprest 12780 lmff 12790 tx1cn 12810 tx2cn 12811 cnblcld 13076 tgioo 13087 reeff1o 13235 pilem1 13241 efhalfpi 13261 coseq0negpitopi 13298 012of 13709 pw1nct 13717 iswomninnlem 13762 |
Copyright terms: Public domain | W3C validator |