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 834 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 834 | . 2 ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜒)) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒))) | |
2 | an12s.1 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) | |
3 | 1, 2 | sylbi 206 | 1 ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜒)) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 |
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 196 df-an 385 |
This theorem is referenced by: anabsan2 859 1stconst 7152 2ndconst 7153 oecl 7504 oaass 7528 odi 7546 oen0 7553 oeworde 7560 ltexprlem4 9740 iccshftr 12177 iccshftl 12179 iccdil 12181 icccntr 12183 ndvdsadd 14972 eulerthlem2 15325 neips 20727 tx1stc 21263 filuni 21499 ufldom 21576 isch3 27482 unoplin 28163 hmoplin 28185 adjlnop 28329 chirredlem2 28634 btwnconn1lem12 31375 btwnconn1 31378 finxpreclem2 32403 poimirlem25 32604 mblfinlem4 32619 iscringd 32967 unichnidl 33000 |
Copyright terms: Public domain | W3C validator |