Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mp3an13 | GIF version |
Description: An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.) |
Ref | Expression |
---|---|
mp3an13.1 | ⊢ 𝜑 |
mp3an13.2 | ⊢ 𝜒 |
mp3an13.3 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
mp3an13 | ⊢ (𝜓 → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mp3an13.1 | . 2 ⊢ 𝜑 | |
2 | mp3an13.2 | . . 3 ⊢ 𝜒 | |
3 | mp3an13.3 | . . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
4 | 2, 3 | mp3an3 1304 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜃) |
5 | 1, 4 | mpan 420 | 1 ⊢ (𝜓 → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 962 |
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 964 |
This theorem is referenced by: pitonnlem1p1 7654 mulid1 7763 addltmul 8956 eluzaddi 9352 fz01en 9833 fznatpl1 9856 expubnd 10350 bernneq 10412 bernneq2 10413 efi4p 11424 efival 11439 cos2tsin 11458 cos01bnd 11465 cos01gt0 11469 dvds0 11508 odd2np1 11570 opoe 11592 gcdid 11674 blssioo 12714 tgioo 12715 rerestcntop 12719 sinperlem 12889 sincosq1sgn 12907 sincosq2sgn 12908 sinq12gt0 12911 cosq14gt0 12913 |
Copyright terms: Public domain | W3C validator |