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 1106 | . 2 |
4 | 1, 3 | mpi 15 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 97 w3a 885 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 df-3an 887 |
This theorem is referenced by: mp3an13 1223 mp3an23 1224 mp3anl3 1228 opelxp 4374 funimaexg 4983 ov 5620 ovmpt2a 5631 ovmpt2 5636 ovtposg 5874 oaword1 6050 th3q 6211 enrefg 6244 f1imaen 6274 addnnnq0 6547 mulnnnq0 6548 prarloclemcalc 6600 genpelxp 6609 genpprecll 6612 genppreclu 6613 addsrpr 6830 mulsrpr 6831 gt0srpr 6833 mulid1 7024 ltneg 7457 leneg 7460 suble0 7471 div1 7680 nnaddcl 7934 nnmulcl 7935 nnge1 7937 nnsub 7952 2halves 8154 halfaddsub 8159 addltmul 8161 zleltp1 8299 nnaddm1cl 8305 zextlt 8332 peano5uzti 8346 eluzp1p1 8498 uzaddcl 8529 znq 8559 xrre 8733 xrre2 8734 fzshftral 8970 expn1ap0 9265 expadd 9297 expmul 9300 expubnd 9311 sqmul 9316 bernneq 9369 sqrecapd 9385 shftval3 9428 caucvgre 9580 leabs 9672 ltabs 9683 caubnd2 9713 nn0seqcvgd 9880 |
Copyright terms: Public domain | W3C validator |