| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Distribution of implication with conjunction (deduction rule). |
| Ref | Expression |
|---|---|
| imdistand.1 |
|
| Ref | Expression |
|---|---|
| imdistand |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | imdistand.1 |
. 2
| |
| 2 | imdistan 442 |
. 2
| |
| 3 | 1, 2 | sylib 198 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: pm5.3 446 fconstfv 3849 unblem1 4540 zorn2lem7 4794 cfub 4908 cflim 4909 prlem936b 5154 suppsr3 5224 supsrlem2 5226 uzss 6431 fsumsplit 7020 climaddc2 7119 cnsscnp 7772 cncnp 7778 ssbl 7855 lmle 7960 ocsh 9156 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 |
| This theorem depends on definitions: df-bi 147 df-an 225 |