![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mp3an2 | Unicode version |
Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.) |
Ref | Expression |
---|---|
mp3an2.1 |
![]() ![]() |
mp3an2.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
mp3an2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mp3an2.1 |
. 2
![]() ![]() | |
2 | mp3an2.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | 3expa 1205 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | mpanl2 435 |
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 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 df-3an 982 |
This theorem is referenced by: mp3anl2 1343 ordin 4403 ordsuc 4580 omv 6479 oeiv 6480 omv2 6489 1idprl 7618 muladd11 8119 negsub 8234 subneg 8235 ltaddneg 8410 muleqadd 8654 diveqap1 8691 conjmulap 8715 nnsub 8987 addltmul 9184 zltp1le 9336 gtndiv 9377 eluzp1m1 9580 xnn0le2is012 9895 divelunit 10031 fznatpl1 10105 flqbi2 10321 flqdiv 10351 frecfzen2 10457 nn0ennn 10463 faclbnd3 10754 shftfvalg 10858 ovshftex 10859 shftfval 10861 abs2dif 11146 cos2t 11789 sin01gt0 11800 cos01gt0 11801 demoivre 11811 demoivreALT 11812 omeo 11934 gcd0id 12011 sqgcd 12061 isprm3 12149 eulerthlemth 12263 pczpre 12328 pcrec 12339 setscom 12551 setsslid 12562 setsslnid 12563 mulgm1 13079 abssinper 14719 lgs1 14898 |
Copyright terms: Public domain | W3C validator |