![]() |
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 1114 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 |
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 1088 |
This theorem is referenced by: oacan 8585 omcan 8606 ecovdi 8864 distrpi 10936 axltadd 11332 ccatlcan 14753 absmulgcd 16583 axlowdimlem14 28985 fh1 31647 fh2 31648 cm2j 31649 hoadddi 31832 hosubdi 31837 leopmul2i 32164 dvconstbi 44330 eel2131 44712 uun2131 44789 uun2131p1 44790 io1ii 48717 reccot 48989 rectan 48990 |
Copyright terms: Public domain | W3C validator |