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

Theorem ancom2s 777
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 436 . 2  |-  ( ( ch  /\  ps )  ->  ( ps  /\  ch ) )
2 an12s.1 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
31, 2sylan2 460 1  |-  ( (
ph  /\  ( ch  /\ 
ps ) )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  an42s  800  sotr2  4343  somin2  5081  xpexr2  5115  f1elima  5787  f1imaeq  5789  soisoi  5825  isosolem  5844  2ndconst  6208  smoword  6383  unxpdomlem3  7069  sornom  7903  fin1a2s  8040  mulsub  9222  leltadd  9258  ltord1  9299  leord1  9300  eqord1  9301  divmul24  9464  expcan  11154  ltexp2  11155  fsum  12193  isprm5  12791  ramub  13060  setcinv  13922  grpidpropd  14399  cmnpropd  15098  unitpropd  15479  lidl1el  15970  ordtrest2  16934  filuni  17580  haustsms2  17819  blcom  17952  metnrmlem3  18365  cnmpt2pc  18426  icoopnst  18437  icccvx  18448  equivcfil  18725  volcn  18961  dvmptfsum  19322  cxple  20042  cxple3  20048  subgoablo  20978  ghablo  21036  lnosub  21337  chirredlem2  22971  gsumpropd2lem  23379  cover2  26358  filbcmb  26432  isdrngo2  26589  crngohomfo  26631  unichnidl  26656  ismrc  26776  gsumcom3  27454  cdleme50eq  30730  dvhvaddcomN  31286
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 177  df-an 360
  Copyright terms: Public domain W3C validator