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 2803 2ordpr 4434 regexmid 4445 ordsoexmid 4472 reg3exmid 4489 intasym 4918 relcoi1 5065 funres11 5190 cnvresid 5192 mpofvex 6094 df1st2 6109 df2nd2 6110 dftpos4 6153 tposf12 6159 frecabcl 6289 xp01disjl 6324 xpcomco 6713 ominf 6783 sbthlem2 6839 djuunr 6944 eldju 6946 ctssdccl 6989 ctssdclemr 6990 omct 6995 ctssexmid 7017 rec1nq 7196 halfnqq 7211 caucvgsrlemasr 7591 axresscn 7661 0re 7759 gtso 7836 cnegexlem2 7931 uzn0 9334 indstr 9381 dfioo2 9750 fnn0nninf 10203 hashinfuni 10516 hashp1i 10549 cnrecnv 10675 rexanuz 10753 xrmaxiflemcom 11011 climdm 11057 sumsnf 11171 tanvalap 11404 egt2lt3 11475 lcmgcdlem 11747 3prm 11798 sqpweven 11842 2sqpwodd 11843 qnumval 11852 qdenval 11853 xpnnen 11896 ennnfonelemhdmp1 11911 ennnfonelemss 11912 ennnfonelemnn0 11924 qnnen 11933 unct 11943 structcnvcnv 11964 setsslid 11998 tgrest 12327 lmbr2 12372 cnptoprest 12397 lmff 12407 tx1cn 12427 tx2cn 12428 cnblcld 12693 tgioo 12704 pilem1 12849 efhalfpi 12869 coseq0negpitopi 12906 isomninnlem 13214 |
Copyright terms: Public domain | W3C validator |