![]() |
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 1207 | . 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) |
4 | 1, 3 | mpi 15 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ∧ w3a 980 |
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 depends on definitions: df-bi 117 df-3an 982 |
This theorem is referenced by: mp3an13 1339 mp3an23 1340 mp3anl3 1344 opelxp 4674 funimaexg 5319 ov 6017 ovmpoa 6028 ovmpo 6033 ovtposg 6285 oaword1 6497 th3q 6667 enrefg 6791 f1imaen 6821 mapxpen 6877 pw1fin 6939 xpfi 6959 djucomen 7246 addnnnq0 7479 mulnnnq0 7480 prarloclemcalc 7532 genpelxp 7541 genpprecll 7544 genppreclu 7545 addsrpr 7775 mulsrpr 7776 gt0srpr 7778 mulrid 7985 ltneg 8450 leneg 8453 suble0 8464 div1 8691 nnaddcl 8970 nnmulcl 8971 nnge1 8973 nnsub 8989 2halves 9179 halfaddsub 9184 addltmul 9186 zleltp1 9339 nnaddm1cl 9345 zextlt 9376 peano5uzti 9392 eluzp1p1 9585 uzaddcl 9618 znq 9656 xrre 9852 xrre2 9853 fzshftral 10140 expn1ap0 10564 expadd 10596 expmul 10599 expubnd 10611 sqmul 10616 bernneq 10675 sqrecapd 10692 faclbnd2 10757 faclbnd6 10759 fihashssdif 10833 shftval3 10871 caucvgre 11025 leabs 11118 ltabs 11131 caubnd2 11161 efexp 11725 efival 11775 cos01gt0 11805 odd2np1 11913 halfleoddlt 11934 omoe 11936 opeo 11937 gcdmultiple 12056 sqgcd 12065 nn0seqcvgd 12076 phiprmpw 12257 eulerthlemth 12267 odzcllem 12277 pcelnn 12356 4sqlem3 12425 lsp0 13756 lss0v 13763 ntrin 14101 txuni2 14233 txopn 14242 xblpnfps 14375 xblpnf 14376 bl2in 14380 unirnblps 14399 unirnbl 14400 blpnfctr 14416 sincosq1eq 14737 rpcxpp1 14804 rplogb1 14843 |
Copyright terms: Public domain | W3C validator |