Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > sylanr1 | Structured version Visualization version GIF version |
Description: A syllogism inference. (Contributed by NM, 9-Apr-2005.) |
Ref | Expression |
---|---|
sylanr1.1 | ⊢ (𝜑 → 𝜒) |
sylanr1.2 | ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜏) |
Ref | Expression |
---|---|
sylanr1 | ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜃)) → 𝜏) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylanr1.1 | . . 3 ⊢ (𝜑 → 𝜒) | |
2 | 1 | anim1i 616 | . 2 ⊢ ((𝜑 ∧ 𝜃) → (𝜒 ∧ 𝜃)) |
3 | sylanr1.2 | . 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜏) | |
4 | 2, 3 | sylan2 594 | 1 ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜃)) → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 |
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 209 df-an 399 |
This theorem is referenced by: adantrll 720 adantrlr 721 sbthlem9 8637 pczpre 16186 cpmadugsumlemF 21486 blsscls2 23116 rpvmasumlem 26065 leopmuli 29912 chirredlem1 30169 chirredlem3 30171 pibt2 34700 dvconstbi 40673 bccbc 40684 reccot 44864 rectan 44865 aacllem 44909 |
Copyright terms: Public domain | W3C validator |