![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mp3an3 | Unicode version |
Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.) |
Ref | Expression |
---|---|
mp3an3.1 |
![]() ![]() |
mp3an3.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
mp3an3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mp3an3.1 |
. 2
![]() ![]() | |
2 | mp3an3.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | 3expia 1184 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | mpi 15 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 965 |
This theorem is referenced by: mp3an13 1307 mp3an23 1308 mp3anl3 1312 opelxp 4577 funimaexg 5215 ov 5898 ovmpoa 5909 ovmpo 5914 ovtposg 6164 oaword1 6375 th3q 6542 enrefg 6666 f1imaen 6696 mapxpen 6750 xpfi 6826 djucomen 7089 addnnnq0 7281 mulnnnq0 7282 prarloclemcalc 7334 genpelxp 7343 genpprecll 7346 genppreclu 7347 addsrpr 7577 mulsrpr 7578 gt0srpr 7580 mulid1 7787 ltneg 8248 leneg 8251 suble0 8262 div1 8487 nnaddcl 8764 nnmulcl 8765 nnge1 8767 nnsub 8783 2halves 8973 halfaddsub 8978 addltmul 8980 zleltp1 9133 nnaddm1cl 9139 zextlt 9167 peano5uzti 9183 eluzp1p1 9375 uzaddcl 9408 znq 9443 xrre 9633 xrre2 9634 fzshftral 9919 expn1ap0 10334 expadd 10366 expmul 10369 expubnd 10381 sqmul 10386 bernneq 10443 sqrecapd 10459 faclbnd2 10520 faclbnd6 10522 fihashssdif 10596 shftval3 10631 caucvgre 10785 leabs 10878 ltabs 10891 caubnd2 10921 efexp 11425 efival 11475 cos01gt0 11505 odd2np1 11606 halfleoddlt 11627 omoe 11629 opeo 11630 gcdmultiple 11744 sqgcd 11753 nn0seqcvgd 11758 phiprmpw 11934 ntrin 12332 txuni2 12464 txopn 12473 xblpnfps 12606 xblpnf 12607 bl2in 12611 unirnblps 12630 unirnbl 12631 blpnfctr 12647 sincosq1eq 12968 rpcxpp1 13035 rplogb1 13073 |
Copyright terms: Public domain | W3C validator |