Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mpdan | Unicode version |
Description: An inference based on modus ponens. (Contributed by NM, 23-May-1999.) (Proof shortened by Wolf Lammen, 22-Nov-2012.) |
Ref | Expression |
---|---|
mpdan.1 | |
mpdan.2 |
Ref | Expression |
---|---|
mpdan |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 19 | . 2 | |
2 | mpdan.1 | . 2 | |
3 | mpdan.2 | . 2 | |
4 | 1, 2, 3 | syl2anc 408 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 107 |
This theorem is referenced by: mpidan 419 mpan2 421 mpjaodan 787 mpd3an3 1316 eueq2dc 2852 csbiegf 3038 difsnb 3658 reusv3i 4375 fvmpt3 5493 ffvelrnd 5549 fnressn 5599 fliftel1 5688 f1oiso2 5721 riota5f 5747 1stvalg 6033 2ndvalg 6034 brtpos2 6141 tfrlemibxssdm 6217 dom2lem 6659 php5 6745 nnfi 6759 xpfi 6811 supisoti 6890 ordiso2 6913 omp1eomlem 6972 onenon 7033 oncardval 7035 cardonle 7036 recidnq 7194 archnqq 7218 prarloclemarch2 7220 recexprlem1ssl 7434 recexprlem1ssu 7435 recexprlemss1l 7436 recexprlemss1u 7437 recexprlemex 7438 0idsr 7568 lep1 8596 suprlubex 8703 uz11 9341 xnegid 9635 eluzfz2 9805 fzsuc 9842 fzsuc2 9852 fzp1disj 9853 fzneuz 9874 fzp1nel 9877 exbtwnzlemex 10020 flhalf 10068 modqval 10090 frec2uzsucd 10167 frecuzrdgsuc 10180 uzsinds 10208 seq3p1 10228 seqp1cd 10232 expubnd 10343 iexpcyc 10390 binom2sub1 10399 hashennn 10519 shftfval 10586 shftcan1 10599 cjval 10610 reval 10614 imval 10615 cjmulrcl 10652 addcj 10656 absval 10766 resqrexlemdecn 10777 resqrexlemnmsq 10782 resqrexlemnm 10783 absneg 10815 abscj 10817 sqabsadd 10820 sqabssub 10821 ltabs 10852 dfabsmax 10982 negfi 10992 fsum3 11149 trirecip 11263 efval 11356 ege2le3 11366 efcan 11371 sinval 11398 cosval 11399 efi4p 11413 resin4p 11414 recos4p 11415 sincossq 11444 eirraplem 11472 iddvds 11495 1dvds 11496 bezoutlemstep 11674 coprmgcdb 11758 1idssfct 11785 exprmfct 11807 oddpwdclemdc 11840 phival 11878 setsn0fun 11985 cldval 12257 ntrfval 12258 clsfval 12259 neifval 12298 tx1cn 12427 ismet 12502 isxmet 12503 divcnap 12713 dvaddxxbr 12823 dvmulxxbr 12824 dvcoapbr 12829 bj-findis 13166 |
Copyright terms: Public domain | W3C validator |