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 869 | . 2 ⊢ (((𝜑 ∧ 𝜑) ∧ (𝜓 ∧ 𝜒)) → 𝜏) |
3 | 2 | anabsan 854 | 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: 3impdi 1381 dff13 6512 f1oiso 6601 omord2 7647 fodomacn 8879 ltapi 9725 ltmpi 9726 axpre-ltadd 9988 faclbnd 13077 pwsdiagmhm 17369 tgcl 20773 brbtwn2 25785 grpoinvf 27386 ocorth 28150 fh1 28477 fh2 28478 spansncvi 28511 lnopmi 28859 adjlnop 28945 matunitlindflem2 33406 poimirlem4 33413 heicant 33444 mblfinlem2 33447 ismblfin 33450 ftc1anclem6 33490 ftc1anclem7 33491 ftc1anc 33493 |
Copyright terms: Public domain | W3C validator |