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

Theorem an12s 648
Description: Swap two conjuncts in antecedent. The label suffix "s" means that an12 644 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 644 . 2 ((𝜓 ∧ (𝜑𝜒)) ↔ (𝜑 ∧ (𝜓𝜒)))
2 an12s.1 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
31, 2sylbi 220 1 ((𝜓 ∧ (𝜑𝜒)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  anabsan2  673  oecl  8149  oaass  8174  odi  8192  oen0  8199  oeworde  8206  ltexprlem4  10450  iccshftr  12864  iccshftl  12866  iccdil  12868  icccntr  12870  ndvdsadd  15750  eulerthlem2  16108  neips  21716  tx1stc  22253  filuni  22488  ufldom  22565  isch3  29022  unoplin  29701  hmoplin  29723  adjlnop  29867  chirredlem2  30172  btwnconn1lem12  33633  btwnconn1  33636  finxpreclem2  34768  poimirlem25  35040  mblfinlem4  35055  iscringd  35394  unichnidl  35427
  Copyright terms: Public domain W3C validator