![]() |
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 6237 2dom 6807 phplem4 6857 fiintim 6930 mulidnq 7390 nq0m0r 7457 nq0a0 7458 addpinq1 7465 0idsr 7768 1idsr 7769 00sr 7770 addresr 7838 mulresr 7839 pitonnlem2 7848 ax0id 7879 recexaplem2 8611 reclt1 8855 crap0 8917 nominpos 9158 expnass 10628 crim 10869 sqrt00 11051 mulcn2 11322 sin02gt0 11773 opoe 11902 oddprm 12261 pythagtriplem3 12269 pc1 12307 txswaphmeo 13860 sinq34lt0t 14291 cosordlem 14309 lgsne0 14478 lgsdinn0 14488 |
Copyright terms: Public domain | W3C validator |