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 1183 | . 2 |
4 | 1, 3 | mpi 15 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 w3a 962 |
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 964 |
This theorem is referenced by: mp3an13 1306 mp3an23 1307 mp3anl3 1311 opelxp 4569 funimaexg 5207 ov 5890 ovmpoa 5901 ovmpo 5906 ovtposg 6156 oaword1 6367 th3q 6534 enrefg 6658 f1imaen 6688 mapxpen 6742 xpfi 6818 djucomen 7072 addnnnq0 7257 mulnnnq0 7258 prarloclemcalc 7310 genpelxp 7319 genpprecll 7322 genppreclu 7323 addsrpr 7553 mulsrpr 7554 gt0srpr 7556 mulid1 7763 ltneg 8224 leneg 8227 suble0 8238 div1 8463 nnaddcl 8740 nnmulcl 8741 nnge1 8743 nnsub 8759 2halves 8949 halfaddsub 8954 addltmul 8956 zleltp1 9109 nnaddm1cl 9115 zextlt 9143 peano5uzti 9159 eluzp1p1 9351 uzaddcl 9381 znq 9416 xrre 9603 xrre2 9604 fzshftral 9888 expn1ap0 10303 expadd 10335 expmul 10338 expubnd 10350 sqmul 10355 bernneq 10412 sqrecapd 10428 faclbnd2 10488 faclbnd6 10490 fihashssdif 10564 shftval3 10599 caucvgre 10753 leabs 10846 ltabs 10859 caubnd2 10889 efexp 11388 efival 11439 cos01gt0 11469 odd2np1 11570 halfleoddlt 11591 omoe 11593 opeo 11594 gcdmultiple 11708 sqgcd 11717 nn0seqcvgd 11722 phiprmpw 11898 ntrin 12293 txuni2 12425 txopn 12434 xblpnfps 12567 xblpnf 12568 bl2in 12572 unirnblps 12591 unirnbl 12592 blpnfctr 12608 sincosq1eq 12920 |
Copyright terms: Public domain | W3C validator |