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

Theorem ancom2s 802
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 449 . 2  |-  ( ( ch  /\  ps )  ->  ( ps  /\  ch ) )
2 an12s.1 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
31, 2sylan2 474 1  |-  ( (
ph  /\  ( ch  /\ 
ps ) )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  an42s  827  sotr2  4819  somin2  5395  f1elima  6156  f1imaeq  6158  soisoi  6209  isosolem  6228  xpexr2  6726  2ndconst  6874  smoword  7039  unxpdomlem3  7728  sornom  8660  fin1a2s  8797  mulsub  10006  leltadd  10043  ltord1  10086  leord1  10087  eqord1  10088  divmul24  10255  expcan  12199  ltexp2  12200  fsum  13523  fprod  13729  isprm5  14234  ramub  14512  setcinv  15395  grpidpropd  15866  gsumpropd2lem  15878  cmnpropd  16785  unitpropd  17324  lidl1el  17844  gsumcom3  18878  1marepvmarrepid  19054  1marepvsma1  19062  ordtrest2  19682  filuni  20363  haustsms2  20612  blcomps  20873  blcom  20874  metnrmlem3  21342  cnmpt2pc  21405  icoopnst  21416  icccvx  21427  equivcfil  21715  volcn  21992  dvmptfsum  22353  cxple  23052  cxple3  23058  subgoablo  25289  ghabloOLD  25347  lnosub  25650  chirredlem2  27286  bhmafibid2  27610  metider  27850  ordtrest2NEW  27882  fin2so  30015  cover2  30179  filbcmb  30206  isdrngo2  30336  crngohomfo  30378  unichnidl  30403  ismrc  30608  cdleme50eq  36007  dvhvaddcomN  36563
  Copyright terms: Public domain W3C validator