![]() |
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 7 |
. 2
![]() ![]() |
4 | mp2b.3 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | ax-mp 7 |
1
![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() |
This theorem was proved from axioms: ax-mp 7 |
This theorem is referenced by: eqvinc 2776 2ordpr 4397 regexmid 4408 ordsoexmid 4435 reg3exmid 4452 intasym 4879 relcoi1 5026 funres11 5151 cnvresid 5153 mpofvex 6053 df1st2 6068 df2nd2 6069 dftpos4 6112 tposf12 6118 frecabcl 6248 xp01disjl 6283 xpcomco 6671 ominf 6741 sbthlem2 6796 djuunr 6901 eldju 6903 ctssdccl 6946 ctssdclemr 6947 ctssexmid 6972 rec1nq 7145 halfnqq 7160 caucvgsrlemasr 7526 axresscn 7589 0re 7684 gtso 7760 cnegexlem2 7855 uzn0 9237 indstr 9284 dfioo2 9644 fnn0nninf 10097 hashinfuni 10410 hashp1i 10443 cnrecnv 10569 rexanuz 10646 xrmaxiflemcom 10904 climdm 10950 sumsnf 11064 tanvalap 11260 egt2lt3 11328 lcmgcdlem 11598 3prm 11649 sqpweven 11692 2sqpwodd 11693 qnumval 11702 qdenval 11703 xpnnen 11746 ennnfonelemhdmp1 11761 ennnfonelemss 11762 ennnfonelemnn0 11774 qnnen 11783 unct 11791 structcnvcnv 11812 setsslid 11846 tgrest 12175 lmbr2 12219 cnptoprest 12244 lmff 12254 tx1cn 12274 tx2cn 12275 cnblcld 12518 tgioo 12526 isomninnlem 12906 |
Copyright terms: Public domain | W3C validator |