![]() |
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 1143 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | mpanl2 426 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 df-3an 926 |
This theorem is referenced by: mp3anl2 1268 ordin 4210 ordsuc 4377 omv 6208 oeiv 6209 omv2 6218 1idprl 7139 muladd11 7605 negsub 7720 subneg 7721 ltaddneg 7892 muleqadd 8127 diveqap1 8162 conjmulap 8186 nnsub 8451 addltmul 8642 zltp1le 8794 gtndiv 8831 eluzp1m1 9032 divelunit 9409 fznatpl1 9478 flqbi2 9686 flqdiv 9716 frecfzen2 9822 nn0ennn 9828 iseqshft2 9886 faclbnd3 10139 shftfvalg 10240 ovshftex 10241 shftfval 10243 abs2dif 10527 cos2t 11028 sin01gt0 11039 cos01gt0 11040 demoivre 11049 demoivreALT 11050 omeo 11163 gcd0id 11235 sqgcd 11283 isprm3 11365 |
Copyright terms: Public domain | W3C validator |