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

Theorem ancom1s 653
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 459 . 2 ((𝜓𝜑) → (𝜑𝜓))
2 an32s.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylan 580 1 (((𝜓𝜑) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395
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 207  df-an 396
This theorem is referenced by:  odi  8616  sornom  10315  leltadd  11745  divmul13  11968  absmax  15365  fzomaxdif  15379  dmatsgrp  22521  comppfsc  23556  iocopnst  24984  mumul  27239  lgsdir2  27389  branmfn  32134  chirredlem2  32420  chirredlem4  32422  icoreclin  37340  relowlssretop  37346  pibt2  37400  frinfm  37722  fzmul  37728  fdc  37732  rpnnen3  43021
  Copyright terms: Public domain W3C validator