![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mp3an23 | GIF version |
Description: An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.) |
Ref | Expression |
---|---|
mp3an23.1 | ⊢ 𝜓 |
mp3an23.2 | ⊢ 𝜒 |
mp3an23.3 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
mp3an23 | ⊢ (𝜑 → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mp3an23.1 | . 2 ⊢ 𝜓 | |
2 | mp3an23.2 | . . 3 ⊢ 𝜒 | |
3 | mp3an23.3 | . . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
4 | 2, 3 | mp3an3 1285 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜃) |
5 | 1, 4 | mpan2 419 | 1 ⊢ (𝜑 → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 943 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 945 |
This theorem is referenced by: sbciegf 2906 ac6sfi 6743 dju0en 7015 1qec 7138 ltaddnq 7157 halfnqq 7160 1idsr 7505 pn0sr 7508 muleqadd 8336 halfcl 8844 rehalfcl 8845 half0 8846 2halves 8847 halfpos2 8848 halfnneg2 8850 halfaddsub 8852 nneoor 9051 zeo 9054 fztp 9745 modqfrac 9997 iexpcyc 10284 bcn2 10397 bcpasc 10399 imre 10510 reim 10511 crim 10517 addcj 10550 imval2 10553 sinf 11256 efi4p 11269 resin4p 11270 recos4p 11271 sinneg 11278 efival 11284 cosadd 11289 sinmul 11296 sinbnd 11304 cosbnd 11305 ef01bndlem 11308 sin01bnd 11309 cos01bnd 11310 sin01gt0 11313 cos01gt0 11314 sin02gt0 11315 odd2np1lem 11411 odd2np1 11412 mopnex 12488 |
Copyright terms: Public domain | W3C validator |