Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > anandirs | Structured version Visualization version GIF version |
Description: Inference that undistributes conjunction in the antecedent. (Contributed by NM, 7-Jun-2004.) |
Ref | Expression |
---|---|
anandirs.1 | ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜒)) → 𝜏) |
Ref | Expression |
---|---|
anandirs | ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜏) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | anandirs.1 | . . 3 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜒)) → 𝜏) | |
2 | 1 | an4s 865 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜒)) → 𝜏) |
3 | 2 | anabsan2 859 | 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 196 df-an 385 |
This theorem is referenced by: 3impdir 1374 oawordri 7517 omwordri 7539 oeordsuc 7561 phplem4 8027 muladd 10341 iccshftr 12177 iccshftl 12179 iccdil 12181 icccntr 12183 fzaddel 12246 fzsubel 12248 modadd1 12569 modmul1 12585 mulexp 12761 faclbnd5 12947 upxp 21236 uptx 21238 brbtwn2 25585 colinearalg 25590 eleesub 25591 eleesubd 25592 axcgrrflx 25594 axcgrid 25596 axsegconlem2 25598 phoeqi 27097 hial2eq2 27348 spansncvi 27895 5oalem3 27899 5oalem5 27901 hoscl 27988 hoeq1 28073 hoeq2 28074 hmops 28263 leopadd 28375 mdsymlem5 28650 lineintmo 31434 matunitlindflem1 32575 heicant 32614 ftc1anclem3 32657 ftc1anclem4 32658 ftc1anclem6 32660 ftc1anclem7 32661 ftc1anclem8 32662 ftc1anc 32663 |
Copyright terms: Public domain | W3C validator |