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 873 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) |
3 | 2 | 3impb 1260 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 384 ∧ w3a 1037 |
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 df-3an 1039 |
This theorem is referenced by: oacan 7628 omcan 7649 ecovdi 7856 distrpi 9720 axltadd 10111 ccatlcan 13472 absmulgcd 15266 axlowdimlem14 25835 fh1 28477 fh2 28478 cm2j 28479 hoadddi 28662 hosubdi 28667 leopmul2i 28994 dvconstbi 38533 eel2131 38939 uun2131 39018 uun2131p1 39019 reccot 42499 rectan 42500 |
Copyright terms: Public domain | W3C validator |