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 464 | . 2 ⊢ ((𝜓 ∧ 𝜑) → (𝜑 ∧ 𝜓)) | |
2 | an32s.1 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | |
3 | 1, 2 | sylan 487 | 1 ⊢ (((𝜓 ∧ 𝜑) ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 |
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 196 df-an 385 |
This theorem is referenced by: odi 7546 sornom 8982 leltadd 10391 divmul13 10607 absmax 13917 fzomaxdif 13931 dmatsgrp 20124 comppfsc 21145 iocopnst 22547 mumul 24707 lgsdir2 24855 branmfn 28348 chirredlem2 28634 chirredlem4 28636 icoreclin 32381 relowlssretop 32387 frinfm 32700 fzmul 32707 fdc 32711 rpnnen3 36617 |
Copyright terms: Public domain | W3C validator |