| 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 645 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 645 | . 2 ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜒)) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒))) | |
| 2 | an12s.1 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) | |
| 3 | 1, 2 | sylbi 217 | 1 ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜒)) → 𝜃) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 |
| 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 207 df-an 396 |
| This theorem is referenced by: anabsan2 674 oecl 8575 oaass 8599 odi 8617 oen0 8624 oeworde 8631 ltexprlem4 11079 iccshftr 13526 iccshftl 13528 iccdil 13530 icccntr 13532 ndvdsadd 16447 eulerthlem2 16819 neips 23121 tx1stc 23658 filuni 23893 ufldom 23970 isch3 31260 unoplin 31939 hmoplin 31961 adjlnop 32105 chirredlem2 32410 btwnconn1lem12 36099 btwnconn1 36102 finxpreclem2 37391 poimirlem25 37652 mblfinlem4 37667 iscringd 38005 unichnidl 38038 |
| Copyright terms: Public domain | W3C validator |