![]() |
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 6234 2dom 6804 phplem4 6854 fiintim 6927 mulidnq 7387 nq0m0r 7454 nq0a0 7455 addpinq1 7462 0idsr 7765 1idsr 7766 00sr 7767 addresr 7835 mulresr 7836 pitonnlem2 7845 ax0id 7876 recexaplem2 8607 reclt1 8851 crap0 8913 nominpos 9154 expnass 10622 crim 10862 sqrt00 11044 mulcn2 11315 sin02gt0 11766 opoe 11894 oddprm 12253 pythagtriplem3 12261 pc1 12299 txswaphmeo 13714 sinq34lt0t 14145 cosordlem 14163 lgsne0 14332 lgsdinn0 14342 |
Copyright terms: Public domain | W3C validator |