![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mp3an1 | GIF version |
Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.) |
Ref | Expression |
---|---|
mp3an1.1 | ⊢ 𝜑 |
mp3an1.2 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
mp3an1 | ⊢ ((𝜓 ∧ 𝜒) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mp3an1.1 | . 2 ⊢ 𝜑 | |
2 | mp3an1.2 | . . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
3 | 2 | 3expb 1204 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) |
4 | 1, 3 | mpan 424 | 1 ⊢ ((𝜓 ∧ 𝜒) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ∧ w3a 978 |
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 980 |
This theorem is referenced by: mp3an12 1327 mp3an1i 1330 mp3anl1 1331 mp3an 1337 mp3an2i 1342 mp3an3an 1343 tfrlem9 6313 rdgexgg 6372 oaexg 6442 omexg 6445 oeiexg 6447 oav2 6457 nnaordex 6522 mulidnq 7366 1idpru 7568 addgt0sr 7752 muladd11 8067 cnegex 8112 negsubdi 8190 renegcl 8195 mulneg1 8329 ltaddpos 8386 addge01 8406 rimul 8519 recclap 8612 recidap 8619 recidap2 8620 recdivap2 8658 divdiv23apzi 8698 ltmul12a 8793 lemul12a 8795 mulgt1 8796 ltmulgt11 8797 gt0div 8803 ge0div 8804 ltdiv23i 8859 8th4div3 9114 gtndiv 9324 nn0ind 9343 fnn0ind 9345 xrre2 9795 ioorebasg 9949 fzen 10016 elfz0ubfz0 10098 expubnd 10550 le2sq2 10568 bernneq 10613 expnbnd 10616 faclbnd6 10695 bccl 10718 hashfacen 10787 shftfval 10801 mulreap 10844 caucvgrelemrec 10959 binom1p 11464 efi4p 11696 sinadd 11715 cosadd 11716 cos2t 11729 cos2tsin 11730 absefib 11749 efieq1re 11750 demoivreALT 11752 odd2np1 11848 opoe 11870 omoe 11871 opeo 11872 omeo 11873 gcdadd 11956 gcdmultiple 11991 algcvgblem 12019 algcvga 12021 isprm3 12088 coprm 12114 1arith2 12336 bl2ioo 13675 ioo2blex 13677 sinperlem 13862 logge0 13934 lgsdir2 14067 1lgs 14077 |
Copyright terms: Public domain | W3C validator |