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  4359  somin2  5097  xpexr2  5131  f1elima  5803  f1imaeq  5805  soisoi  5841  isosolem  5860  2ndconst  6224  smoword  6399  unxpdomlem3  7085  sornom  7919  fin1a2s  8056  mulsub  9238  leltadd  9274  ltord1  9315  leord1  9316  eqord1  9317  divmul24  9480  expcan  11170  ltexp2  11171  fsum  12209  isprm5  12807  ramub  13076  setcinv  13938  grpidpropd  14415  cmnpropd  15114  unitpropd  15495  lidl1el  15986  ordtrest2  16950  filuni  17596  haustsms2  17835  blcom  17968  metnrmlem3  18381  cnmpt2pc  18442  icoopnst  18453  icccvx  18464  equivcfil  18741  volcn  18977  dvmptfsum  19338  cxple  20058  cxple3  20064  subgoablo  20994  ghablo  21052  lnosub  21353  chirredlem2  22987  gsumpropd2lem  23394  fprod  24164  cover2  26461  filbcmb  26535  isdrngo2  26692  crngohomfo  26734  unichnidl  26759  ismrc  26879  gsumcom3  27557  cdleme50eq  31352  dvhvaddcomN  31908
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