![]() |
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 1202 | . . 3 ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏))) |
4 | 1, 3 | syl7 69 | . 2 ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜏))) |
5 | 4 | 3imp 1193 | 1 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ 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: syl3an3b 1276 syl3an3br 1279 vtoclgft 2789 ovmpox 6006 ovmpoga 6007 nnanq0 7460 apreim 8563 apsub1 8602 divassap 8650 ltmul2 8816 xleadd1 9878 xltadd2 9880 elfzo 10152 fzodcel 10155 subcn2 11322 mulcn2 11323 ndvdsp1 11940 gcddiv 12023 lcmneg 12077 mulgaddcom 13013 lspsnss 13496 neipsm 13794 opnneip 13799 hmeof1o2 13948 blcntrps 14055 blcntr 14056 neibl 14131 blnei 14132 metss 14134 rpcxpsub 14469 cxpcom 14497 rplogbzexp 14512 |
Copyright terms: Public domain | W3C validator |