Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mpanl12 | Unicode version |
Description: An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.) |
Ref | Expression |
---|---|
mpanl12.1 | |
mpanl12.2 | |
mpanl12.3 |
Ref | Expression |
---|---|
mpanl12 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpanl12.2 | . 2 | |
2 | mpanl12.1 | . . 3 | |
3 | mpanl12.3 | . . 3 | |
4 | 2, 3 | mpanl1 430 | . 2 |
5 | 1, 4 | mpan 420 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 |
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 is referenced by: reuun1 3358 ordtri2orexmid 4438 opthreg 4471 ordtri2or2exmid 4486 fvtp1 5631 nq0m0r 7264 nq02m 7273 gt0srpr 7556 map2psrprg 7613 pitoregt0 7657 axcnre 7689 addgt0 8210 addgegt0 8211 addgtge0 8212 addge0 8213 addgt0i 8250 addge0i 8251 addgegt0i 8252 add20i 8254 mulge0i 8382 recextlem1 8412 recap0 8445 recdivap 8478 recgt1 8655 prodgt0i 8666 prodge0i 8667 iccshftri 9778 iccshftli 9780 iccdili 9782 icccntri 9784 mulexpzap 10333 expaddzap 10337 m1expeven 10340 iexpcyc 10397 amgm2 10890 ege2le3 11377 sqnprm 11816 lmres 12417 |
Copyright terms: Public domain | W3C validator |