![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mp3an12 | GIF version |
Description: An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.) |
Ref | Expression |
---|---|
mp3an12.1 | ⊢ 𝜑 |
mp3an12.2 | ⊢ 𝜓 |
mp3an12.3 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
mp3an12 | ⊢ (𝜒 → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mp3an12.2 | . 2 ⊢ 𝜓 | |
2 | mp3an12.1 | . . 3 ⊢ 𝜑 | |
3 | mp3an12.3 | . . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
4 | 2, 3 | mp3an1 1267 | . 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃) |
5 | 1, 4 | mpan 416 | 1 ⊢ (𝜒 → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 927 |
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 929 |
This theorem is referenced by: mp3an12i 1284 ceqsralv 2664 brelrn 4700 funpr 5100 fpm 6478 ener 6576 ltaddnq 7063 ltadd1sr 7419 mul02 7962 ltapi 8208 div0ap 8266 divclapzi 8311 divcanap1zi 8312 divcanap2zi 8313 divrecapzi 8314 divcanap3zi 8315 divcanap4zi 8316 divassapzi 8326 divmulapzi 8327 divdirapzi 8328 redivclapzi 8342 ltm1 8404 mulgt1 8421 recgt1i 8456 recreclt 8458 ltmul1i 8478 ltdiv1i 8479 ltmuldivi 8480 ltmul2i 8481 lemul1i 8482 lemul2i 8483 cju 8519 nnge1 8543 nngt0 8545 nnrecgt0 8558 elnnnn0c 8816 elnnz1 8871 recnz 8938 eluzsubi 9145 ge0gtmnf 9389 m1expcl2 10092 1exp 10099 m1expeven 10117 expubnd 10127 iexpcyc 10174 expnbnd 10192 expnlbnd 10193 remim 10409 imval2 10443 cjdivapi 10484 absdivapzi 10702 ef01bndlem 11196 sin01gt0 11201 cos01gt0 11202 absefib 11209 efieq1re 11210 zeo3 11295 evend2 11316 cnbl0 12311 |
Copyright terms: Public domain | W3C validator |