![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mp3an2 | GIF version |
Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.) |
Ref | Expression |
---|---|
mp3an2.1 | ⊢ 𝜓 |
mp3an2.2 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
mp3an2 | ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mp3an2.1 | . 2 ⊢ 𝜓 | |
2 | mp3an2.2 | . . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
3 | 2 | 3expa 1149 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
4 | 1, 3 | mpanl2 429 | 1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 930 |
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 932 |
This theorem is referenced by: mp3anl2 1278 ordin 4245 ordsuc 4416 omv 6281 oeiv 6282 omv2 6291 1idprl 7299 muladd11 7766 negsub 7881 subneg 7882 ltaddneg 8053 muleqadd 8290 diveqap1 8326 conjmulap 8350 nnsub 8617 addltmul 8808 zltp1le 8960 gtndiv 8998 eluzp1m1 9199 xnn0le2is012 9490 divelunit 9626 fznatpl1 9697 flqbi2 9905 flqdiv 9935 frecfzen2 10041 nn0ennn 10047 faclbnd3 10330 shftfvalg 10431 ovshftex 10432 shftfval 10434 abs2dif 10718 cos2t 11255 sin01gt0 11266 cos01gt0 11267 demoivre 11276 demoivreALT 11277 omeo 11390 gcd0id 11462 sqgcd 11510 isprm3 11592 setscom 11781 setsslid 11791 setsslnid 11792 |
Copyright terms: Public domain | W3C validator |