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

Theorem an12s 647
Description: Swap two conjuncts in antecedent. The label suffix "s" means that an12 643 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 643 . 2 ((𝜓 ∧ (𝜑𝜒)) ↔ (𝜑 ∧ (𝜓𝜒)))
2 an12s.1 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
31, 2sylbi 216 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 206  df-an 397
This theorem is referenced by:  anabsan2  672  oecl  8519  oaass  8544  odi  8562  oen0  8569  oeworde  8576  ltexprlem4  11016  iccshftr  13445  iccshftl  13447  iccdil  13449  icccntr  13451  ndvdsadd  16335  eulerthlem2  16697  neips  22546  tx1stc  23083  filuni  23318  ufldom  23395  isch3  30357  unoplin  31036  hmoplin  31058  adjlnop  31202  chirredlem2  31507  btwnconn1lem12  34900  btwnconn1  34903  finxpreclem2  36075  poimirlem25  36317  mblfinlem4  36332  iscringd  36671  unichnidl  36704
  Copyright terms: Public domain W3C validator