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 327 | . 2 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜒))) |
3 | 2 | imp 123 | 1 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem is referenced by: xoranor 1359 nfan1 1544 sbcof2 1790 difin 3344 difrab 3381 opthreg 4515 wessep 4537 fvelimab 5524 elfvmptrab 5563 dffo4 5615 dffo5 5616 ltaddpr 7517 recgt1i 8769 elnnnn0c 9135 elnnz1 9190 recnz 9257 eluz2b2 9514 elfzp12 10001 cos01gt0 11659 oddnn02np1 11770 bj-charfundc 13383 |
Copyright terms: Public domain | W3C validator |