![]() |
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 1205 |
. 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 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 df-3an 980 |
This theorem is referenced by: mp3an13 1328 mp3an23 1329 mp3anl3 1333 opelxp 4653 funimaexg 5296 ov 5988 ovmpoa 5999 ovmpo 6004 ovtposg 6254 oaword1 6466 th3q 6634 enrefg 6758 f1imaen 6788 mapxpen 6842 pw1fin 6904 xpfi 6923 djucomen 7209 addnnnq0 7439 mulnnnq0 7440 prarloclemcalc 7492 genpelxp 7501 genpprecll 7504 genppreclu 7505 addsrpr 7735 mulsrpr 7736 gt0srpr 7738 mulid1 7945 ltneg 8409 leneg 8412 suble0 8423 div1 8649 nnaddcl 8928 nnmulcl 8929 nnge1 8931 nnsub 8947 2halves 9137 halfaddsub 9142 addltmul 9144 zleltp1 9297 nnaddm1cl 9303 zextlt 9334 peano5uzti 9350 eluzp1p1 9542 uzaddcl 9575 znq 9613 xrre 9807 xrre2 9808 fzshftral 10094 expn1ap0 10516 expadd 10548 expmul 10551 expubnd 10563 sqmul 10568 bernneq 10626 sqrecapd 10643 faclbnd2 10706 faclbnd6 10708 fihashssdif 10782 shftval3 10820 caucvgre 10974 leabs 11067 ltabs 11080 caubnd2 11110 efexp 11674 efival 11724 cos01gt0 11754 odd2np1 11861 halfleoddlt 11882 omoe 11884 opeo 11885 gcdmultiple 12004 sqgcd 12013 nn0seqcvgd 12024 phiprmpw 12205 eulerthlemth 12215 odzcllem 12225 pcelnn 12303 4sqlem3 12371 ntrin 13291 txuni2 13423 txopn 13432 xblpnfps 13565 xblpnf 13566 bl2in 13570 unirnblps 13589 unirnbl 13590 blpnfctr 13606 sincosq1eq 13927 rpcxpp1 13994 rplogb1 14033 |
Copyright terms: Public domain | W3C validator |