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

Theorem ancom1s 842
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 463 . 2 ((𝜓𝜑) → (𝜑𝜓))
2 an32s.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylan 486 1 (((𝜓𝜑) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  odi  7520  sornom  8956  leltadd  10358  divmul13  10574  absmax  13860  fzomaxdif  13874  dmatsgrp  20063  comppfsc  21084  iocopnst  22475  mumul  24621  lgsdir2  24769  branmfn  28151  chirredlem2  28437  chirredlem4  28439  icoreclin  32181  relowlssretop  32187  frinfm  32500  fzmul  32507  fdc  32511  rpnnen3  36417
  Copyright terms: Public domain W3C validator