| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > mpanr2 | Unicode version | ||
| Description: An inference based on modus ponens. (Contributed by NM, 3-May-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 7-Apr-2013.) |
| Ref | Expression |
|---|---|
| mpanr2.1 |
|
| mpanr2.2 |
|
| Ref | Expression |
|---|---|
| mpanr2 |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mpanr2.1 |
. . 3
| |
| 2 | 1 | jctr 315 |
. 2
|
| 3 | mpanr2.2 |
. 2
| |
| 4 | 2, 3 | sylan2 286 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
| This theorem is referenced by: op1steq 6265 fpmg 6761 pmresg 6763 pw2f1odc 6932 pm54.43 7298 prarloclemarch2 7532 prarloclemlt 7606 prsradd 7899 muleqadd 8741 divdivap1 8796 addltmul 9274 elfzp1b 10219 elfzm1b 10220 expp1zap 10733 expm1ap 10734 fiinbas 14521 opnneissb 14627 blssec 14910 |
| Copyright terms: Public domain | W3C validator |