![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > an12s | Structured version Visualization version GIF version |
Description: Swap two conjuncts in antecedent. The label suffix "s" means that an12 644 is combined with syl 17 (or a variant). (Contributed by NM, 13-Mar-1996.) |
Ref | Expression |
---|---|
an12s.1 | ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) |
Ref | Expression |
---|---|
an12s | ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜒)) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | an12 644 | . 2 ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜒)) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒))) | |
2 | an12s.1 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) | |
3 | 1, 2 | sylbi 216 | 1 ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜒)) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 |
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 206 df-an 398 |
This theorem is referenced by: anabsan2 673 oecl 8537 oaass 8561 odi 8579 oen0 8586 oeworde 8593 ltexprlem4 11034 iccshftr 13463 iccshftl 13465 iccdil 13467 icccntr 13469 ndvdsadd 16353 eulerthlem2 16715 neips 22617 tx1stc 23154 filuni 23389 ufldom 23466 isch3 30525 unoplin 31204 hmoplin 31226 adjlnop 31370 chirredlem2 31675 btwnconn1lem12 35101 btwnconn1 35104 finxpreclem2 36319 poimirlem25 36561 mblfinlem4 36576 iscringd 36914 unichnidl 36947 |
Copyright terms: Public domain | W3C validator |