![]() |
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 1141 | . 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) |
4 | 1, 3 | mpi 15 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 ∧ w3a 920 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 df-3an 922 |
This theorem is referenced by: mp3an13 1260 mp3an23 1261 mp3anl3 1265 opelxp 4394 funimaexg 5008 ov 5645 ovmpt2a 5656 ovmpt2 5661 ovtposg 5902 oaword1 6108 th3q 6270 enrefg 6303 f1imaen 6333 addnnnq0 6690 mulnnnq0 6691 prarloclemcalc 6743 genpelxp 6752 genpprecll 6755 genppreclu 6756 addsrpr 6973 mulsrpr 6974 gt0srpr 6976 mulid1 7167 ltneg 7622 leneg 7625 suble0 7636 div1 7847 nnaddcl 8115 nnmulcl 8116 nnge1 8118 nnsub 8133 2halves 8316 halfaddsub 8321 addltmul 8323 zleltp1 8476 nnaddm1cl 8482 zextlt 8509 peano5uzti 8525 eluzp1p1 8714 uzaddcl 8744 znq 8779 xrre 8952 xrre2 8953 fzshftral 9190 expn1ap0 9572 expadd 9604 expmul 9607 expubnd 9619 sqmul 9624 bernneq 9679 sqrecapd 9695 faclbnd2 9755 faclbnd6 9757 shftval3 9842 caucvgre 9994 leabs 10087 ltabs 10100 caubnd2 10130 odd2np1 10406 halfleoddlt 10427 omoe 10429 opeo 10430 gcdmultiple 10542 sqgcd 10551 nn0seqcvgd 10556 |
Copyright terms: Public domain | W3C validator |