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

Theorem ancom1s 781
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 437 . 2  |-  ( ( ps  /\  ph )  ->  ( ph  /\  ps ) )
2 an32s.1 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
31, 2sylan 458 1  |-  ( ( ( ps  /\  ph )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  odi  6758  sornom  8090  leltadd  9444  divmul13  9649  absmax  12060  fzomaxdif  12074  iocopnst  18836  mumul  20831  lgsdir2  20979  branmfn  23456  chirredlem2  23742  chirredlem4  23744  comppfsc  26078  frinfm  26128  fzmul  26135  fdc  26140  rpnnen3  26794  unxpwdom3  26925
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