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

Theorem an12s 649
Description: Swap two conjuncts in antecedent. The label suffix "s" means that an12 645 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 645 . 2 ((𝜓 ∧ (𝜑𝜒)) ↔ (𝜑 ∧ (𝜓𝜒)))
2 an12s.1 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
31, 2sylbi 217 1 ((𝜓 ∧ (𝜑𝜒)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395
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 207  df-an 396
This theorem is referenced by:  anabsan2  674  oecl  8575  oaass  8599  odi  8617  oen0  8624  oeworde  8631  ltexprlem4  11079  iccshftr  13526  iccshftl  13528  iccdil  13530  icccntr  13532  ndvdsadd  16447  eulerthlem2  16819  neips  23121  tx1stc  23658  filuni  23893  ufldom  23970  isch3  31260  unoplin  31939  hmoplin  31961  adjlnop  32105  chirredlem2  32410  btwnconn1lem12  36099  btwnconn1  36102  finxpreclem2  37391  poimirlem25  37652  mblfinlem4  37667  iscringd  38005  unichnidl  38038
  Copyright terms: Public domain W3C validator