![]() |
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: ![]() |
This theorem was proved from axioms: ax-mp 5 |
This theorem is referenced by: eqvinc 2875 2ordpr 4541 regexmid 4552 ordsoexmid 4579 reg3exmid 4597 intasym 5031 relcoi1 5178 funres11 5307 cnvresid 5309 mpofvex 6228 df1st2 6244 df2nd2 6245 dftpos4 6288 tposf12 6294 frecabcl 6424 xp01disjl 6459 xpcomco 6852 ominf 6924 sbthlem2 6987 djuunr 7095 eldju 7097 ctssdccl 7140 ctssdclemr 7141 omct 7146 ctssexmid 7178 rec1nq 7424 halfnqq 7439 caucvgsrlemasr 7819 axresscn 7889 0re 7987 gtso 8066 cnegexlem2 8163 uzn0 9573 indstr 9623 dfioo2 10004 fnn0nninf 10468 hashinfuni 10789 hashp1i 10822 cnrecnv 10951 rexanuz 11029 xrmaxiflemcom 11289 climdm 11335 sumsnf 11449 tanvalap 11748 egt2lt3 11819 lcmgcdlem 12109 3prm 12160 sqpweven 12207 2sqpwodd 12208 qnumval 12217 qdenval 12218 xpnnen 12445 ennnfonelemhdmp1 12460 ennnfonelemss 12461 ennnfonelemnn0 12473 qnnen 12482 ctiunctal 12492 unct 12493 structcnvcnv 12528 setsslid 12563 xpsfrn 12826 xpsff1o2 12827 ringn0 13412 rmodislmodlem 13666 cnfldsub 13878 cnsubmlem 13881 cnsubglem 13882 zring0 13899 tgrest 14126 lmbr2 14171 cnptoprest 14196 lmff 14206 tx1cn 14226 tx2cn 14227 cnblcld 14492 tgioo 14503 reeff1o 14651 pilem1 14657 efhalfpi 14677 coseq0negpitopi 14714 012of 15204 pw1nct 15211 iswomninnlem 15256 |
Copyright terms: Public domain | W3C validator |