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

Theorem ancom1s 846
 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 465 . 2 ((𝜓𝜑) → (𝜑𝜓))
2 an32s.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylan 488 1 (((𝜓𝜑) ∧ 𝜒) → 𝜃)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384 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 197  df-an 386 This theorem is referenced by:  odi  7644  sornom  9084  leltadd  10497  divmul13  10713  absmax  14050  fzomaxdif  14064  dmatsgrp  20286  comppfsc  21316  iocopnst  22720  mumul  24888  lgsdir2  25036  branmfn  28934  chirredlem2  29220  chirredlem4  29222  icoreclin  33176  relowlssretop  33182  frinfm  33501  fzmul  33508  fdc  33512  rpnnen3  37418
 Copyright terms: Public domain W3C validator