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 322 | . 2 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜒))) |
3 | 2 | imp 122 | 1 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem is referenced by: xoranor 1308 nfan1 1496 sbcof2 1731 difin 3201 difrab 3238 opthreg 4299 wessep 4320 fvelimab 5250 dffo4 5336 dffo5 5337 ltaddpr 6787 recgt1i 7976 elnnnn0c 8333 elnnz1 8374 recnz 8440 eluz2b2 8690 elfzp12 9116 oddnn02np1 10280 |
Copyright terms: Public domain | W3C validator |