![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > imdistani | GIF version |
Description: Distribution of implication with conjunction. (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
imdistani.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
imdistani | ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imdistani.1 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | 1 | anc2li 329 | . 2 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜒))) |
3 | 2 | imp 124 | 1 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem is referenced by: syldanl 449 xoranor 1377 nfan1 1564 sbcof2 1810 difin 3372 difrab 3409 opthreg 4555 wessep 4577 fvelimab 5572 elfvmptrab 5611 dffo4 5664 dffo5 5665 ltaddpr 7595 recgt1i 8853 elnnnn0c 9219 elnnz1 9274 recnz 9344 eluz2b2 9601 elfzp12 10096 cos01gt0 11765 oddnn02np1 11879 reumodprminv 12247 sgrpidmndm 12775 bj-charfundc 14442 |
Copyright terms: Public domain | W3C validator |