Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > syld3an1 | Structured version Visualization version GIF version |
Description: A syllogism inference. (Contributed by NM, 7-Jul-2008.) |
Ref | Expression |
---|---|
syld3an1.1 | ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜑) |
syld3an1.2 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏) |
Ref | Expression |
---|---|
syld3an1 | ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜏) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syld3an1.1 | . . . 4 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜑) | |
2 | 1 | 3com13 1262 | . . 3 ⊢ ((𝜃 ∧ 𝜓 ∧ 𝜒) → 𝜑) |
3 | syld3an1.2 | . . . 4 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏) | |
4 | 3 | 3com13 1262 | . . 3 ⊢ ((𝜃 ∧ 𝜓 ∧ 𝜑) → 𝜏) |
5 | 2, 4 | syld3an3 1363 | . 2 ⊢ ((𝜃 ∧ 𝜓 ∧ 𝜒) → 𝜏) |
6 | 5 | 3com13 1262 | 1 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1031 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 196 df-an 385 df-3an 1033 |
This theorem is referenced by: npncan 10181 nnpcan 10183 ppncan 10202 muldivdir 10599 div2neg 10627 ltmuldiv 10775 opfi1uzind 13138 opfi1uzindOLD 13144 sgrp2nmndlem4 17238 zndvds 19717 subdivcomb1 30864 wsuceq123 31004 atlrelat1 33626 cvlatcvr1 33646 dih11 35572 mullimc 38683 mullimcf 38690 icccncfext 38773 stoweidlem34 38927 stoweidlem49 38942 stoweidlem57 38950 sigarexp 39697 el0ldepsnzr 42050 |
Copyright terms: Public domain | W3C validator |