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

Theorem ancom1s 780
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
an32s.1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Assertion
Ref Expression
ancom1s  |-  ( ( ( ps  /\  ph )  /\  ch )  ->  th )

Proof of Theorem ancom1s
StepHypRef Expression
1 pm3.22 436 . 2  |-  ( ( ps  /\  ph )  ->  ( ph  /\  ps ) )
2 an32s.1 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
31, 2sylan 457 1  |-  ( ( ( ps  /\  ph )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  odi  6577  sornom  7903  leltadd  9258  divmul13  9463  absmax  11813  fzomaxdif  11827  iocopnst  18438  mumul  20419  lgsdir2  20567  branmfn  22685  chirredlem2  22971  chirredlem4  22973  comppfsc  26307  frinfm  26416  fzmul  26443  fdc  26455  rpnnen3  27125  unxpwdom3  27256
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