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 463 . 2 ((𝜓𝜑) → (𝜑𝜓))
2 an32s.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylan 583 1 (((𝜓𝜑) ∧ 𝜒) → 𝜃)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399 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 210  df-an 400 This theorem is referenced by:  odi  8220  sornom  9742  leltadd  11167  divmul13  11386  absmax  14742  fzomaxdif  14756  dmatsgrp  21204  comppfsc  22237  iocopnst  23646  mumul  25870  lgsdir2  26018  branmfn  29992  chirredlem2  30278  chirredlem4  30280  icoreclin  35080  relowlssretop  35086  pibt2  35140  frinfm  35479  fzmul  35485  fdc  35489  rpnnen3  40374
 Copyright terms: Public domain W3C validator