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

Theorem ancom1s 812
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 450 . 2  |-  ( ( ps  /\  ph )  ->  ( ph  /\  ps ) )
2 an32s.1 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
31, 2sylan 473 1  |-  ( ( ( ps  /\  ph )  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  odi  7279  sornom  8696  leltadd  10087  divmul13  10299  absmax  13360  fzomaxdif  13374  dmatsgrp  19448  comppfsc  20471  iocopnst  21857  mumul  23968  lgsdir2  24116  branmfn  27590  chirredlem2  27876  chirredlem4  27878  icoreclin  31491  relowlssretop  31497  frinfm  31766  fzmul  31773  fdc  31778  rpnnen3  35597
  Copyright terms: Public domain W3C validator