| 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 678 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) |
| 3 | 2 | 3impb 1115 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 |
| 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 df-3an 1089 |
| This theorem is referenced by: oacan 8586 omcan 8607 ecovdi 8865 distrpi 10938 axltadd 11334 ccatlcan 14756 absmulgcd 16586 axlowdimlem14 28970 fh1 31637 fh2 31638 cm2j 31639 hoadddi 31822 hosubdi 31827 leopmul2i 32154 dvconstbi 44353 eel2131 44734 uun2131 44811 uun2131p1 44812 io1ii 48818 reccot 49277 rectan 49278 |
| Copyright terms: Public domain | W3C validator |