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 465 | . 2 ⊢ ((𝜓 ∧ 𝜑) → (𝜑 ∧ 𝜓)) | |
2 | an32s.1 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | |
3 | 1, 2 | sylan 488 | 1 ⊢ (((𝜓 ∧ 𝜑) ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 384 |
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 197 df-an 386 |
This theorem is referenced by: odi 7659 sornom 9099 leltadd 10512 divmul13 10728 absmax 14069 fzomaxdif 14083 dmatsgrp 20305 comppfsc 21335 iocopnst 22739 mumul 24907 lgsdir2 25055 branmfn 28964 chirredlem2 29250 chirredlem4 29252 icoreclin 33205 relowlssretop 33211 frinfm 33530 fzmul 33537 fdc 33541 rpnnen3 37599 |
Copyright terms: Public domain | W3C validator |