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 432 | . 2 |
5 | 1, 4 | mpan 422 | 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 3409 ordtri2orexmid 4505 opthreg 4538 ordtri2or2exmid 4553 ontri2orexmidim 4554 fvtp1 5704 nq0m0r 7405 nq02m 7414 gt0srpr 7697 map2psrprg 7754 pitoregt0 7798 axcnre 7830 addgt0 8354 addgegt0 8355 addgtge0 8356 addge0 8357 addgt0i 8394 addge0i 8395 addgegt0i 8396 add20i 8398 mulge0i 8526 recextlem1 8556 recap0 8589 recdivap 8622 recgt1 8800 prodgt0i 8811 prodge0i 8812 iccshftri 9939 iccshftli 9941 iccdili 9943 icccntri 9945 mulexpzap 10503 expaddzap 10507 m1expeven 10510 iexpcyc 10567 amgm2 11069 ege2le3 11621 sqnprm 12077 lmres 12963 2logb9irrap 13610 |
Copyright terms: Public domain | W3C validator |