| 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 660 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜒)) → 𝜏) |
| 3 | 2 | anabsan2 674 | 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 207 df-an 396 |
| This theorem is referenced by: 3impdir 1352 oawordri 8588 omwordri 8610 oeordsuc 8632 phplem2 9245 phplem4OLD 9257 muladd 11695 iccshftr 13526 iccshftl 13528 iccdil 13530 icccntr 13532 fzaddel 13598 fzsubel 13600 modadd1 13948 modmul1 13965 mulexp 14142 faclbnd5 14337 upxp 23631 uptx 23633 brbtwn2 28920 colinearalg 28925 eleesub 28926 eleesubd 28927 axcgrrflx 28929 axcgrid 28931 axsegconlem2 28933 phoeqi 30876 hial2eq2 31126 spansncvi 31671 5oalem3 31675 5oalem5 31677 hoscl 31764 hoeq1 31849 hoeq2 31850 hmops 32039 leopadd 32151 mdsymlem5 32426 lineintmo 36158 matunitlindflem1 37623 heicant 37662 ftc1anclem3 37702 ftc1anclem4 37703 ftc1anclem6 37705 ftc1anclem7 37706 ftc1anclem8 37707 ftc1anc 37708 |
| Copyright terms: Public domain | W3C validator |