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

Theorem ancom1s 803
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 449 . 2  |-  ( ( ps  /\  ph )  ->  ( ph  /\  ps ) )
2 an32s.1 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
31, 2sylan 471 1  |-  ( ( ( ps  /\  ph )  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  odi  7017  sornom  8445  leltadd  9822  divmul13  10033  absmax  12816  fzomaxdif  12830  iocopnst  20511  mumul  22518  lgsdir2  22666  branmfn  25508  chirredlem2  25794  chirredlem4  25796  comppfsc  28577  frinfm  28627  fzmul  28634  fdc  28639  rpnnen3  29379  dmatsgrp  30876  scmatsgrp  30883
  Copyright terms: Public domain W3C validator