Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  an12s Structured version   Visualization version   GIF version

Theorem an12s 839
 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.)
Hypothesis
Ref Expression
an12s.1 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
Assertion
Ref Expression
an12s ((𝜓 ∧ (𝜑𝜒)) → 𝜃)

Proof of Theorem an12s
StepHypRef Expression
1 an12 834 . 2 ((𝜓 ∧ (𝜑𝜒)) ↔ (𝜑 ∧ (𝜓𝜒)))
2 an12s.1 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
31, 2sylbi 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