![]() |
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 659 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜒)) → 𝜏) |
3 | 2 | anabsan2 673 | 1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 |
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 398 |
This theorem is referenced by: 3impdir 1352 oawordri 8546 omwordri 8568 oeordsuc 8590 phplem2 9204 phplem4OLD 9216 muladd 11642 iccshftr 13459 iccshftl 13461 iccdil 13463 icccntr 13465 fzaddel 13531 fzsubel 13533 modadd1 13869 modmul1 13885 mulexp 14063 faclbnd5 14254 upxp 23109 uptx 23111 brbtwn2 28143 colinearalg 28148 eleesub 28149 eleesubd 28150 axcgrrflx 28152 axcgrid 28154 axsegconlem2 28156 phoeqi 30088 hial2eq2 30338 spansncvi 30883 5oalem3 30887 5oalem5 30889 hoscl 30976 hoeq1 31061 hoeq2 31062 hmops 31251 leopadd 31363 mdsymlem5 31638 lineintmo 35067 matunitlindflem1 36422 heicant 36461 ftc1anclem3 36501 ftc1anclem4 36502 ftc1anclem6 36504 ftc1anclem7 36505 ftc1anclem8 36506 ftc1anc 36507 |
Copyright terms: Public domain | W3C validator |