| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > syl3an3 | GIF version | ||
| Description: A syllogism inference. (Contributed by NM, 22-Aug-1995.) |
| Ref | Expression |
|---|---|
| syl3an3.1 | ⊢ (𝜑 → 𝜃) |
| syl3an3.2 | ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) |
| Ref | Expression |
|---|---|
| syl3an3 | ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | syl3an3.1 | . . 3 ⊢ (𝜑 → 𝜃) | |
| 2 | syl3an3.2 | . . . 4 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) | |
| 3 | 2 | 3exp 1228 | . . 3 ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏))) |
| 4 | 1, 3 | syl7 69 | . 2 ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜏))) |
| 5 | 4 | 3imp 1219 | 1 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏) |
| Colors of variables: wff set class |
| Syntax hints: → wi 4 ∧ w3a 1004 |
| 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 1006 |
| This theorem is referenced by: syl3an3b 1311 syl3an3br 1314 vtoclgft 2854 ovmpox 6150 ovmpoga 6151 nnanq0 7678 apreim 8783 apsub1 8822 divassap 8870 ltmul2 9036 xleadd1 10110 xltadd2 10112 elfzo 10384 fzodcel 10388 subcn2 11889 mulcn2 11890 ndvdsp1 12511 gcddiv 12608 lcmneg 12664 mulgaddcom 13751 lspsnss 14437 rnglidlrng 14531 neipsm 14897 opnneip 14902 hmeof1o2 15051 blcntrps 15158 blcntr 15159 neibl 15234 blnei 15235 metss 15237 rpcxpsub 15651 cxpcom 15681 rplogbzexp 15697 konigsbergssiedgwpren 16355 |
| Copyright terms: Public domain | W3C validator |