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 4507 opthreg 4540 ordtri2or2exmid 4555 ontri2orexmidim 4556 fvtp1 5707 nq0m0r 7418 nq02m 7427 gt0srpr 7710 map2psrprg 7767 pitoregt0 7811 axcnre 7843 addgt0 8367 addgegt0 8368 addgtge0 8369 addge0 8370 addgt0i 8407 addge0i 8408 addgegt0i 8409 add20i 8411 mulge0i 8539 recextlem1 8569 recap0 8602 recdivap 8635 recgt1 8813 prodgt0i 8824 prodge0i 8825 iccshftri 9952 iccshftli 9954 iccdili 9956 icccntri 9958 mulexpzap 10516 expaddzap 10520 m1expeven 10523 iexpcyc 10580 amgm2 11082 ege2le3 11634 sqnprm 12090 lmres 13042 2logb9irrap 13689 |
Copyright terms: Public domain | W3C validator |