![]() |
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 886 | . 2 ⊢ (((𝜑 ∧ 𝜑) ∧ (𝜓 ∧ 𝜒)) → 𝜏) |
3 | 2 | anabsan 871 | 1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 |
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 385 |
This theorem is referenced by: 3impdi 1421 dff13 6552 f1oiso 6641 omord2 7692 fodomacn 8917 ltapi 9763 ltmpi 9764 axpre-ltadd 10026 faclbnd 13117 pwsdiagmhm 17416 tgcl 20821 brbtwn2 25830 grpoinvf 27514 ocorth 28278 fh1 28605 fh2 28606 spansncvi 28639 lnopmi 28987 adjlnop 29073 matunitlindflem2 33536 poimirlem4 33543 heicant 33574 mblfinlem2 33577 ismblfin 33580 ftc1anclem6 33620 ftc1anclem7 33621 ftc1anc 33623 |
Copyright terms: Public domain | W3C validator |