![]() |
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 659 | . 2 ⊢ (((𝜑 ∧ 𝜑) ∧ (𝜓 ∧ 𝜒)) → 𝜏) |
3 | 2 | anabsan 664 | 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 1348 dff13 7259 f1oiso 7353 omord2 8581 fodomacn 10071 ltapi 10918 ltmpi 10919 axpre-ltadd 11182 faclbnd 14273 pwsdiagmhm 18774 tgcl 22859 brbtwn2 28703 grpoinvf 30329 ocorth 31088 fh1 31415 fh2 31416 spansncvi 31449 lnopmi 31797 adjlnop 31883 matunitlindflem2 37025 poimirlem4 37032 heicant 37063 mblfinlem2 37066 ismblfin 37069 ftc1anclem6 37106 ftc1anclem7 37107 ftc1anc 37109 |
Copyright terms: Public domain | W3C validator |