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 1200 | . 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) |
4 | 1, 3 | mpi 15 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 973 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 975 |
This theorem is referenced by: mp3an13 1323 mp3an23 1324 mp3anl3 1328 opelxp 4639 funimaexg 5280 ov 5969 ovmpoa 5980 ovmpo 5985 ovtposg 6235 oaword1 6447 th3q 6614 enrefg 6738 f1imaen 6768 mapxpen 6822 pw1fin 6884 xpfi 6903 djucomen 7180 addnnnq0 7398 mulnnnq0 7399 prarloclemcalc 7451 genpelxp 7460 genpprecll 7463 genppreclu 7464 addsrpr 7694 mulsrpr 7695 gt0srpr 7697 mulid1 7904 ltneg 8368 leneg 8371 suble0 8382 div1 8607 nnaddcl 8885 nnmulcl 8886 nnge1 8888 nnsub 8904 2halves 9094 halfaddsub 9099 addltmul 9101 zleltp1 9254 nnaddm1cl 9260 zextlt 9291 peano5uzti 9307 eluzp1p1 9499 uzaddcl 9532 znq 9570 xrre 9764 xrre2 9765 fzshftral 10051 expn1ap0 10473 expadd 10505 expmul 10508 expubnd 10520 sqmul 10525 bernneq 10583 sqrecapd 10600 faclbnd2 10663 faclbnd6 10665 fihashssdif 10740 shftval3 10778 caucvgre 10932 leabs 11025 ltabs 11038 caubnd2 11068 efexp 11632 efival 11682 cos01gt0 11712 odd2np1 11819 halfleoddlt 11840 omoe 11842 opeo 11843 gcdmultiple 11962 sqgcd 11971 nn0seqcvgd 11982 phiprmpw 12163 eulerthlemth 12173 odzcllem 12183 pcelnn 12261 4sqlem3 12329 ntrin 12839 txuni2 12971 txopn 12980 xblpnfps 13113 xblpnf 13114 bl2in 13118 unirnblps 13137 unirnbl 13138 blpnfctr 13154 sincosq1eq 13475 rpcxpp1 13542 rplogb1 13581 |
Copyright terms: Public domain | W3C validator |