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

Theorem ancom1s 814
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 451 . 2  |-  ( ( ps  /\  ph )  ->  ( ph  /\  ps ) )
2 an32s.1 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
31, 2sylan 474 1  |-  ( ( ( ps  /\  ph )  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 189  df-an 373
This theorem is referenced by:  odi  7280  sornom  8707  leltadd  10098  divmul13  10310  absmax  13392  fzomaxdif  13406  dmatsgrp  19524  comppfsc  20547  iocopnst  21968  mumul  24108  lgsdir2  24256  branmfn  27758  chirredlem2  28044  chirredlem4  28046  icoreclin  31760  relowlssretop  31766  frinfm  32062  fzmul  32069  fdc  32074  rpnnen3  35887
  Copyright terms: Public domain W3C validator