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

Theorem an12s 878
Description: Swap two conjuncts in antecedent. The label suffix "s" means that an12 873 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 873 . 2 ((𝜓 ∧ (𝜑𝜒)) ↔ (𝜑 ∧ (𝜓𝜒)))
2 an12s.1 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
31, 2sylbi 207 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 197  df-an 385
This theorem is referenced by:  anabsan2  898  1stconst  7434  2ndconst  7435  oecl  7788  oaass  7812  odi  7830  oen0  7837  oeworde  7844  ltexprlem4  10073  iccshftr  12519  iccshftl  12521  iccdil  12523  icccntr  12525  ndvdsadd  15356  eulerthlem2  15709  neips  21139  tx1stc  21675  filuni  21910  ufldom  21987  isch3  28428  unoplin  29109  hmoplin  29131  adjlnop  29275  chirredlem2  29580  btwnconn1lem12  32532  btwnconn1  32535  finxpreclem2  33556  poimirlem25  33765  mblfinlem4  33780  iscringd  34128  unichnidl  34161
  Copyright terms: Public domain W3C validator