Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mpanr12 | GIF version |
Description: An inference based on modus ponens. (Contributed by NM, 24-Jul-2009.) |
Ref | Expression |
---|---|
mpanr12.1 | ⊢ 𝜓 |
mpanr12.2 | ⊢ 𝜒 |
mpanr12.3 | ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) |
Ref | Expression |
---|---|
mpanr12 | ⊢ (𝜑 → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpanr12.2 | . 2 ⊢ 𝜒 | |
2 | mpanr12.1 | . . 3 ⊢ 𝜓 | |
3 | mpanr12.3 | . . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) | |
4 | 2, 3 | mpanr1 433 | . 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
5 | 1, 4 | mpan2 421 | 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: cnvoprab 6099 2dom 6667 phplem4 6717 fiintim 6785 mulidnq 7165 nq0m0r 7232 nq0a0 7233 addpinq1 7240 0idsr 7543 1idsr 7544 00sr 7545 addresr 7613 mulresr 7614 pitonnlem2 7623 ax0id 7654 recexaplem2 8381 reclt1 8622 crap0 8684 nominpos 8925 expnass 10366 crim 10598 sqrt00 10780 mulcn2 11049 sin02gt0 11397 opoe 11519 txswaphmeo 12417 sinq34lt0t 12839 cosordlem 12857 |
Copyright terms: Public domain | W3C validator |