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  7228  sornom  8657  leltadd  10036  divmul13  10247  absmax  13125  fzomaxdif  13139  dmatsgrp  18796  iocopnst  21203  mumul  23211  lgsdir2  23359  branmfn  26728  chirredlem2  27014  chirredlem4  27016  comppfsc  29807  frinfm  29857  fzmul  29864  fdc  29869  rpnnen3  30606
  Copyright terms: Public domain W3C validator