|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > ancom1s | Structured version Visualization version GIF version | ||
| Description: Inference commuting a nested conjunction in antecedent. (Contributed by NM, 24-May-2006.) (Proof shortened by Wolf Lammen, 24-Nov-2012.) | 
| Ref | Expression | 
|---|---|
| an32s.1 | ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | 
| Ref | Expression | 
|---|---|
| ancom1s | ⊢ (((𝜓 ∧ 𝜑) ∧ 𝜒) → 𝜃) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | pm3.22 459 | . 2 ⊢ ((𝜓 ∧ 𝜑) → (𝜑 ∧ 𝜓)) | |
| 2 | an32s.1 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | |
| 3 | 1, 2 | sylan 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 8618 sornom 10318 leltadd 11748 divmul13 11971 absmax 15369 fzomaxdif 15383 dmatsgrp 22506 comppfsc 23541 iocopnst 24971 mumul 27225 lgsdir2 27375 branmfn 32125 chirredlem2 32411 chirredlem4 32413 icoreclin 37359 relowlssretop 37365 pibt2 37419 frinfm 37743 fzmul 37749 fdc 37753 rpnnen3 43049 | 
| Copyright terms: Public domain | W3C validator |