MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ancom2s Structured version   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  4524  somin2  5264  xpexr2  5300  f1elima  6001  f1imaeq  6003  soisoi  6040  isosolem  6059  2ndconst  6428  smoword  6620  unxpdomlem3  7307  sornom  8149  fin1a2s  8286  mulsub  9468  leltadd  9504  ltord1  9545  leord1  9546  eqord1  9547  divmul24  9710  expcan  11424  ltexp2  11425  fsum  12506  isprm5  13104  ramub  13373  setcinv  14237  grpidpropd  14714  cmnpropd  15413  unitpropd  15794  lidl1el  16281  ordtrest2  17260  filuni  17909  haustsms2  18158  blcomps  18415  blcom  18416  metnrmlem3  18883  cnmpt2pc  18945  icoopnst  18956  icccvx  18967  equivcfil  19244  volcn  19490  dvmptfsum  19851  cxple  20578  cxple3  20584  subgoablo  21891  ghablo  21949  lnosub  22252  chirredlem2  23886  gsumpropd2lem  24212  metider  24281  fprod  25259  cover2  26396  filbcmb  26423  isdrngo2  26555  crngohomfo  26597  unichnidl  26622  ismrc  26736  gsumcom3  27412  2cshwcom  28220  cdleme50eq  31265  dvhvaddcomN  31821
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