![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > anandis | Structured version Visualization version GIF version |
Description: Inference that undistributes conjunction in the antecedent. (Contributed by NM, 7-Jun-2004.) |
Ref | Expression |
---|---|
anandis.1 | ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)) → 𝜏) |
Ref | Expression |
---|---|
anandis | ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜏) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | anandis.1 | . . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)) → 𝜏) | |
2 | 1 | an4s 657 | . 2 ⊢ (((𝜑 ∧ 𝜑) ∧ (𝜓 ∧ 𝜒)) → 𝜏) |
3 | 2 | anabsan 662 | 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 206 df-an 396 |
This theorem is referenced by: 3impdi 1349 dff13 7257 f1oiso 7351 omord2 8573 fodomacn 10057 ltapi 10904 ltmpi 10905 axpre-ltadd 11168 faclbnd 14257 pwsdiagmhm 18751 tgcl 22705 brbtwn2 28445 grpoinvf 30067 ocorth 30826 fh1 31153 fh2 31154 spansncvi 31187 lnopmi 31535 adjlnop 31621 matunitlindflem2 36801 poimirlem4 36808 heicant 36839 mblfinlem2 36842 ismblfin 36845 ftc1anclem6 36882 ftc1anclem7 36883 ftc1anc 36885 |
Copyright terms: Public domain | W3C validator |