![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3impdi | Structured version Visualization version GIF version |
Description: Importation inference (undistribute conjunction). (Contributed by NM, 14-Aug-1995.) |
Ref | Expression |
---|---|
3impdi.1 | ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)) → 𝜃) |
Ref | Expression |
---|---|
3impdi | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3impdi.1 | . . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)) → 𝜃) | |
2 | 1 | anandis 677 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) |
3 | 2 | 3impb 1113 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1085 |
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 396 df-3an 1087 |
This theorem is referenced by: oacan 8562 omcan 8583 ecovdi 8835 distrpi 10913 axltadd 11309 ccatlcan 14692 absmulgcd 16516 axlowdimlem14 28753 fh1 31415 fh2 31416 cm2j 31417 hoadddi 31600 hosubdi 31605 leopmul2i 31932 dvconstbi 43694 eel2131 44076 uun2131 44153 uun2131p1 44154 io1ii 47862 reccot 48112 rectan 48113 |
Copyright terms: Public domain | W3C validator |