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

Theorem ancom1s 805
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
Assertion
Ref Expression
ancom1s

Proof of Theorem ancom1s
StepHypRef Expression
1 pm3.22 449 . 2
2 an32s.1 . 2
31, 2sylan 471 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  odi  7247  sornom  8678  leltadd  10061  divmul13  10272  absmax  13162  fzomaxdif  13176  dmatsgrp  19001  comppfsc  20033  iocopnst  21440  mumul  23455  lgsdir2  23603  branmfn  27024  chirredlem2  27310  chirredlem4  27312  frinfm  30226  fzmul  30233  fdc  30238  rpnnen3  30974
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
  Copyright terms: Public domain W3C validator