MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ancom2s Unicode version

Theorem ancom2s 778
Description: Inference commuting a nested conjunction in antecedent. (Contributed by NM, 24-May-2006.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
Hypothesis
Ref Expression
an12s.1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
Assertion
Ref Expression
ancom2s  |-  ( (
ph  /\  ( ch  /\ 
ps ) )  ->  th )

Proof of Theorem ancom2s
StepHypRef Expression
1 pm3.22 437 . 2  |-  ( ( ch  /\  ps )  ->  ( ps  /\  ch ) )
2 an12s.1 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
31, 2sylan2 461 1  |-  ( (
ph  /\  ( ch  /\ 
ps ) )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  an42s  801  sotr2  4475  somin2  5214  xpexr2  5250  f1elima  5950  f1imaeq  5952  soisoi  5989  isosolem  6008  2ndconst  6377  smoword  6566  unxpdomlem3  7253  sornom  8092  fin1a2s  8229  mulsub  9410  leltadd  9446  ltord1  9487  leord1  9488  eqord1  9489  divmul24  9652  expcan  11361  ltexp2  11362  fsum  12443  isprm5  13041  ramub  13310  setcinv  14174  grpidpropd  14651  cmnpropd  15350  unitpropd  15731  lidl1el  16218  ordtrest2  17192  filuni  17840  haustsms2  18089  blcom  18328  metnrmlem3  18764  cnmpt2pc  18826  icoopnst  18837  icccvx  18848  equivcfil  19125  volcn  19367  dvmptfsum  19728  cxple  20455  cxple3  20461  subgoablo  21749  ghablo  21807  lnosub  22110  chirredlem2  23744  gsumpropd2lem  24051  fprod  25048  cover2  26108  filbcmb  26135  isdrngo2  26267  crngohomfo  26309  unichnidl  26334  ismrc  26448  gsumcom3  27125  cdleme50eq  30657  dvhvaddcomN  31213
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator