![]() |
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 460 | . 2 ⊢ ((𝜓 ∧ 𝜑) → (𝜑 ∧ 𝜓)) | |
2 | an32s.1 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | |
3 | 1, 2 | sylan 580 | 1 ⊢ (((𝜓 ∧ 𝜑) ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 |
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 397 |
This theorem is referenced by: odi 8581 sornom 10274 leltadd 11700 divmul13 11919 absmax 15278 fzomaxdif 15292 dmatsgrp 22008 comppfsc 23043 iocopnst 24463 mumul 26692 lgsdir2 26840 branmfn 31396 chirredlem2 31682 chirredlem4 31684 icoreclin 36324 relowlssretop 36330 pibt2 36384 frinfm 36689 fzmul 36695 fdc 36699 rpnnen3 41853 |
Copyright terms: Public domain | W3C validator |