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

Theorem an12s 645
Description: Swap two conjuncts in antecedent. The label suffix "s" means that an12 641 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 641 . 2 ((𝜓 ∧ (𝜑𝜒)) ↔ (𝜑 ∧ (𝜓𝜒)))
2 an12s.1 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
31, 2sylbi 218 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 208  df-an 397
This theorem is referenced by:  anabsan2  670  oecl  8151  oaass  8176  odi  8194  oen0  8201  oeworde  8208  ltexprlem4  10449  iccshftr  12860  iccshftl  12862  iccdil  12864  icccntr  12866  ndvdsadd  15749  eulerthlem2  16107  neips  21649  tx1stc  22186  filuni  22421  ufldom  22498  isch3  28945  unoplin  29624  hmoplin  29646  adjlnop  29790  chirredlem2  30095  btwnconn1lem12  33456  btwnconn1  33459  finxpreclem2  34553  poimirlem25  34798  mblfinlem4  34813  iscringd  35157  unichnidl  35190
  Copyright terms: Public domain W3C validator