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 676 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) |
3 | 2 | 3impb 1111 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 ∧ w3a 1083 |
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 209 df-an 399 df-3an 1085 |
This theorem is referenced by: oacan 8176 omcan 8197 ecovdi 8407 distrpi 10322 axltadd 10716 ccatlcan 14082 absmulgcd 15899 axlowdimlem14 26743 fh1 29397 fh2 29398 cm2j 29399 hoadddi 29582 hosubdi 29587 leopmul2i 29914 dvconstbi 40673 eel2131 41055 uun2131 41132 uun2131p1 41133 reccot 44864 rectan 44865 |
Copyright terms: Public domain | W3C validator |