![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mp3an3 | GIF version |
Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.) |
Ref | Expression |
---|---|
mp3an3.1 | ⊢ 𝜒 |
mp3an3.2 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
mp3an3 | ⊢ ((𝜑 ∧ 𝜓) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mp3an3.1 | . 2 ⊢ 𝜒 | |
2 | mp3an3.2 | . . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
3 | 2 | 3expia 1166 | . 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) |
4 | 1, 3 | mpi 15 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 945 |
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 947 |
This theorem is referenced by: mp3an13 1289 mp3an23 1290 mp3anl3 1294 opelxp 4529 funimaexg 5165 ov 5844 ovmpoa 5855 ovmpo 5860 ovtposg 6110 oaword1 6321 th3q 6488 enrefg 6612 f1imaen 6642 mapxpen 6695 xpfi 6771 djucomen 7020 addnnnq0 7205 mulnnnq0 7206 prarloclemcalc 7258 genpelxp 7267 genpprecll 7270 genppreclu 7271 addsrpr 7488 mulsrpr 7489 gt0srpr 7491 mulid1 7687 ltneg 8143 leneg 8146 suble0 8157 div1 8376 nnaddcl 8650 nnmulcl 8651 nnge1 8653 nnsub 8669 2halves 8853 halfaddsub 8858 addltmul 8860 zleltp1 9013 nnaddm1cl 9019 zextlt 9047 peano5uzti 9063 eluzp1p1 9253 uzaddcl 9283 znq 9318 xrre 9496 xrre2 9497 fzshftral 9781 expn1ap0 10196 expadd 10228 expmul 10231 expubnd 10243 sqmul 10248 bernneq 10305 sqrecapd 10321 faclbnd2 10381 faclbnd6 10383 fihashssdif 10457 shftval3 10492 caucvgre 10645 leabs 10738 ltabs 10751 caubnd2 10781 efexp 11239 efival 11290 cos01gt0 11320 odd2np1 11418 halfleoddlt 11439 omoe 11441 opeo 11442 gcdmultiple 11554 sqgcd 11563 nn0seqcvgd 11568 phiprmpw 11743 ntrin 12136 txuni2 12267 txopn 12276 xblpnfps 12387 xblpnf 12388 bl2in 12392 unirnblps 12411 unirnbl 12412 blpnfctr 12428 |
Copyright terms: Public domain | W3C validator |