Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mpanl1 | Unicode version |
Description: An inference based on modus ponens. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Wolf Lammen, 7-Apr-2013.) |
Ref | Expression |
---|---|
mpanl1.1 | |
mpanl1.2 |
Ref | Expression |
---|---|
mpanl1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpanl1.1 | . . 3 | |
2 | 1 | jctl 307 | . 2 |
3 | mpanl1.2 | . 2 | |
4 | 2, 3 | sylan 277 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 102 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem is referenced by: mpanl12 426 ercnv 6150 rec11api 7841 divdiv23apzi 7853 recp1lt1 7977 divgt0i 7988 divge0i 7989 ltreci 7990 lereci 7991 lt2msqi 7992 le2msqi 7993 msq11i 7994 ltdiv23i 8004 fnn0ind 8463 elfzp1b 9114 elfzm1b 9115 sqrt11i 10018 sqrtmuli 10019 sqrtmsq2i 10021 sqrtlei 10022 sqrtlti 10023 |
Copyright terms: Public domain | W3C validator |