![]() |
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 437 | . 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
5 | 1, 4 | mpan2 425 | 1 ⊢ (𝜑 → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 |
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: cnvoprab 6289 2dom 6861 phplem4 6913 fiintim 6987 mulidnq 7451 nq0m0r 7518 nq0a0 7519 addpinq1 7526 0idsr 7829 1idsr 7830 00sr 7831 addresr 7899 mulresr 7900 pitonnlem2 7909 ax0id 7940 recexaplem2 8673 reclt1 8917 crap0 8979 nominpos 9223 expnass 10719 crim 11005 sqrt00 11187 mulcn2 11458 sin02gt0 11910 opoe 12039 oddprm 12400 pythagtriplem3 12408 pc1 12446 txswaphmeo 14500 sinq34lt0t 15007 cosordlem 15025 lgsne0 15195 lgsdinn0 15205 |
Copyright terms: Public domain | W3C validator |