![]() |
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 461 | . 2 ⊢ ((𝜓 ∧ 𝜑) → (𝜑 ∧ 𝜓)) | |
2 | an32s.1 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | |
3 | 1, 2 | sylan 581 | 1 ⊢ (((𝜓 ∧ 𝜑) ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 |
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 206 df-an 398 |
This theorem is referenced by: odi 8579 sornom 10272 leltadd 11698 divmul13 11917 absmax 15276 fzomaxdif 15290 dmatsgrp 22001 comppfsc 23036 iocopnst 24456 mumul 26685 lgsdir2 26833 branmfn 31358 chirredlem2 31644 chirredlem4 31646 icoreclin 36238 relowlssretop 36244 pibt2 36298 frinfm 36603 fzmul 36609 fdc 36613 rpnnen3 41771 |
Copyright terms: Public domain | W3C validator |