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 641 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 641 | . 2 ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜒)) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒))) | |
2 | an12s.1 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) | |
3 | 1, 2 | sylbi 218 | 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 208 df-an 397 |
This theorem is referenced by: anabsan2 670 oecl 8151 oaass 8176 odi 8194 oen0 8201 oeworde 8208 ltexprlem4 10449 iccshftr 12860 iccshftl 12862 iccdil 12864 icccntr 12866 ndvdsadd 15749 eulerthlem2 16107 neips 21649 tx1stc 22186 filuni 22421 ufldom 22498 isch3 28945 unoplin 29624 hmoplin 29646 adjlnop 29790 chirredlem2 30095 btwnconn1lem12 33456 btwnconn1 33459 finxpreclem2 34553 poimirlem25 34798 mblfinlem4 34813 iscringd 35157 unichnidl 35190 |
Copyright terms: Public domain | W3C validator |