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

Theorem ancom1s 652
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 461 . 2 ((𝜓𝜑) → (𝜑𝜓))
2 an32s.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylan 581 1 (((𝜓𝜑) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 206  df-an 398
This theorem is referenced by:  odi  8579  sornom  10272  leltadd  11698  divmul13  11917  absmax  15276  fzomaxdif  15290  dmatsgrp  22001  comppfsc  23036  iocopnst  24456  mumul  26685  lgsdir2  26833  branmfn  31358  chirredlem2  31644  chirredlem4  31646  icoreclin  36238  relowlssretop  36244  pibt2  36298  frinfm  36603  fzmul  36609  fdc  36613  rpnnen3  41771
  Copyright terms: Public domain W3C validator