![]() |
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 643 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 643 | . 2 ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜒)) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒))) | |
2 | an12s.1 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) | |
3 | 1, 2 | sylbi 216 | 1 ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜒)) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 |
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 397 |
This theorem is referenced by: anabsan2 672 oecl 8519 oaass 8544 odi 8562 oen0 8569 oeworde 8576 ltexprlem4 11016 iccshftr 13445 iccshftl 13447 iccdil 13449 icccntr 13451 ndvdsadd 16335 eulerthlem2 16697 neips 22546 tx1stc 23083 filuni 23318 ufldom 23395 isch3 30357 unoplin 31036 hmoplin 31058 adjlnop 31202 chirredlem2 31507 btwnconn1lem12 34900 btwnconn1 34903 finxpreclem2 36075 poimirlem25 36317 mblfinlem4 36332 iscringd 36671 unichnidl 36704 |
Copyright terms: Public domain | W3C validator |